Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impexp | GIF version |
Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
Ref | Expression |
---|---|
impexp | ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.3 248 | . 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | |
2 | pm3.31 249 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒)) | |
3 | 1, 2 | impbii 117 | 1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: imp4a 331 exp4a 348 imdistan 418 pm5.3 444 pm4.87 493 nan 626 pm4.14dc 787 pm5.6dc 835 2sb6 1860 2sb6rf 1866 2exsb 1885 mor 1942 eu2 1944 moanim 1974 r2alf 2341 r3al 2366 r19.23t 2423 ceqsralt 2581 ralrab 2702 ralrab2 2706 euind 2728 reu2 2729 reu3 2731 rmo4 2734 reuind 2744 rmo2ilem 2847 rmo3 2849 ralss 3006 rabss 3017 raldifb 3083 unissb 3610 elintrab 3627 ssintrab 3638 dftr5 3857 repizf2lem 3914 reusv3 4192 tfi 4305 raliunxp 4477 fununi 4967 dff13 5407 dfsmo2 5902 qliftfun 6188 prime 8337 raluz 8521 raluz2 8522 ralrp 8604 bdcriota 10003 |
Copyright terms: Public domain | W3C validator |