![]() |
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 261 | . 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | |
2 | pm3.31 262 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒)) | |
3 | 1, 2 | impbii 126 | 1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: imp4a 349 exp4a 366 imdistan 444 pm5.3 475 pm4.87 557 nan 692 pm4.14dc 890 pm5.6dc 926 2sb6 1984 2sb6rf 1990 2exsb 2009 mor 2068 eu2 2070 moanim 2100 r2alf 2494 r3al 2521 r19.23t 2584 ceqsralt 2764 rspc2gv 2853 ralrab 2898 ralrab2 2902 euind 2924 reu2 2925 reu3 2927 rmo4 2930 rmo3f 2934 reuind 2942 rmo2ilem 3052 rmo3 3054 ralss 3221 rabss 3232 raldifb 3275 unissb 3839 elintrab 3856 ssintrab 3867 dftr5 4104 repizf2lem 4161 reusv3 4460 tfi 4581 raliunxp 4768 fununi 5284 dff13 5768 dfsmo2 6287 tfr1onlemaccex 6348 tfrcllemaccex 6361 qliftfun 6616 nnnninfeq2 7126 prime 9351 raluz 9577 raluz2 9578 ralrp 9674 facwordi 10719 modfsummod 11465 nnwosdc 12039 isprm2 12116 isprm4 12118 metcnp 13982 limcdifap 14101 bdcriota 14605 |
Copyright terms: Public domain | W3C validator |