| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > impexp | Structured version Visualization version GIF version | ||
| Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
| Ref | Expression |
|---|---|
| impexp | ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm3.3 448 | . 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | |
| 2 | pm3.31 449 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒)) | |
| 3 | 1, 2 | impbii 209 | 1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: imdistan 567 pm4.14 807 nan 830 pm4.87 844 pm5.6 1004 2sb6 2086 r2allem 3142 r3al 3197 r19.23t 3255 moelOLD 3405 ceqsralt 3516 rspc2gv 3632 ralrab 3699 ralrab2 3704 euind 3730 reu2 3731 reu3 3733 rmo4 3736 rmo3f 3740 reuind 3759 2reu5lem3 3763 rmo2 3887 rmo3 3889 rmoanim 3894 rmoanimALT 3895 ralss 4058 ralssOLD 4060 rabss 4072 raldifb 4149 ralin 4249 rabsssn 4668 raldifsni 4795 unissb 4939 unissbOLD 4940 elintrab 4960 ssintrab 4971 dftr5 5263 dftr5OLD 5264 axrep5 5287 reusv2lem4 5401 reusv2 5403 reusv3 5405 raliunxp 5850 dfpo2 6316 fununi 6641 fvn0ssdmfun 7094 dff13 7275 ordunisuc2 7865 dfom2 7889 frpoins3xpg 8165 frpoins3xp3g 8166 xpord2indlem 8172 xpord3inddlem 8179 dfsmo2 8387 qliftfun 8842 dfsup2 9484 wemapsolem 9590 iscard2 10016 acnnum 10092 aceq1 10157 dfac9 10177 dfacacn 10182 axgroth6 10868 sstskm 10882 infm3 12227 prime 12699 raluz 12938 raluz2 12939 nnwos 12957 ralrp 13055 facwordi 14328 cotr2g 15015 rexuzre 15391 limsupgle 15513 ello12 15552 elo12 15563 lo1resb 15600 rlimresb 15601 o1resb 15602 modfsummod 15830 isprm2 16719 isprm4 16721 isprm7 16745 acsfn2 17706 pgpfac1 20100 isirred2 20421 isdomn2OLD 20712 isdomn3 20715 islindf4 21858 coe1fzgsumd 22308 evl1gsumd 22361 ist1-2 23355 isnrm2 23366 dfconn2 23427 1stccn 23471 iskgen3 23557 hausdiag 23653 cnflf 24010 txflf 24014 cnfcf 24050 metcnp 24554 caucfil 25317 ovolgelb 25515 ismbl 25561 dyadmbllem 25634 itg2leub 25769 ellimc3 25914 mdegleb 26103 jensen 27032 dchrelbas2 27281 dchrelbas3 27282 eqscut2 27851 nmoubi 30791 nmobndseqi 30798 nmobndseqiALT 30799 h1dei 31569 nmopub 31927 nmfnleub 31944 mdsl1i 32340 mdsl2i 32341 elat2 32359 rabsspr 32520 rabsstp 32521 islinds5 33395 islbs5 33408 eulerpartlemgvv 34378 bnj115 34739 bnj1109 34800 bnj1533 34866 bnj580 34927 bnj864 34936 bnj865 34937 bnj1049 34988 bnj1090 34993 bnj1093 34994 bnj1133 35003 bnj1171 35014 climuzcnv 35676 axextprim 35701 biimpexp 35717 dfon2lem8 35791 dffun10 35915 filnetlem4 36382 bj-substax12 36722 wl-2sb6d 37559 poimirlem25 37652 poimirlem30 37657 r2alan 38250 inxpss 38312 moantr 38365 isat3 39308 isltrn2N 40122 cdlemefrs29bpre0 40398 cdleme32fva 40439 sn-axrep5v 42255 dford4 43041 fnwe2lem2 43063 ifpidg 43504 ifpim23g 43508 elmapintrab 43589 undmrnresiss 43617 df3or2 43781 df3an2 43782 dfhe3 43788 dffrege76 43952 dffrege115 43991 ntrneiiso 44104 ismnushort 44320 pm11.62 44413 2sbc6g 44434 expcomdg 44520 impexpd 44533 dfvd2 44599 dfvd3 44611 modelac8prim 45009 rabssf 45124 2rexsb 47113 2rexrsb 47114 snlindsntor 48388 elbigo2 48473 exp12bd 48716 ralbidb 48720 ralbidc 48721 |
| Copyright terms: Public domain | W3C validator |