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 450 | . 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | |
2 | pm3.31 451 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒)) | |
3 | 1, 2 | impbii 208 | 1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: imdistan 569 pm4.14 806 nan 829 pm4.87 842 pm5.6 1001 2sb6 2090 r2allem 3138 r3al 3192 r19.23t 3237 moelOLD 3377 ceqsralt 3475 rspc2gv 3588 ralrab 3650 ralrab2 3655 euind 3681 reu2 3682 reu3 3684 rmo4 3687 rmo3f 3691 reuind 3710 2reu5lem3 3714 rmo2 3842 rmo3 3844 rmoanim 3849 rmoanimALT 3850 ralss 4013 rabss 4028 raldifb 4103 rabsssn 4627 raldifsni 4754 unissb 4899 unissbOLD 4900 elintrab 4920 ssintrab 4931 dftr5 5225 dftr5OLD 5226 axrep5 5247 reusv2lem4 5355 reusv2 5357 reusv3 5359 raliunxp 5792 dfpo2 6245 fununi 6572 fvn0ssdmfun 7021 dff13 7197 ordunisuc2 7771 dfom2 7795 dfsmo2 8261 qliftfun 8675 dfsup2 9314 wemapsolem 9420 iscard2 9846 acnnum 9922 aceq1 9987 dfac9 10006 dfacacn 10011 axgroth6 10698 sstskm 10712 infm3 12048 prime 12515 raluz 12750 raluz2 12751 nnwos 12769 ralrp 12864 facwordi 14117 cotr2g 14795 rexuzre 15172 limsupgle 15294 ello12 15333 elo12 15344 lo1resb 15381 rlimresb 15382 o1resb 15383 modfsummod 15614 isprm2 16493 isprm4 16495 isprm7 16519 acsfn2 17478 pgpfac1 19789 isirred2 20054 isdomn2 20693 islindf4 21168 coe1fzgsumd 21596 evl1gsumd 21646 ist1-2 22621 isnrm2 22632 dfconn2 22693 1stccn 22737 iskgen3 22823 hausdiag 22919 cnflf 23276 txflf 23280 cnfcf 23316 metcnp 23820 caucfil 24570 ovolgelb 24767 ismbl 24813 dyadmbllem 24886 itg2leub 25022 ellimc3 25166 mdegleb 25352 jensen 26261 dchrelbas2 26508 dchrelbas3 26509 eqscut2 27068 nmoubi 29513 nmobndseqi 29520 nmobndseqiALT 29521 h1dei 30291 nmopub 30649 nmfnleub 30666 mdsl1i 31062 mdsl2i 31063 elat2 31081 islinds5 31950 eulerpartlemgvv 32750 bnj115 33111 bnj1109 33172 bnj1533 33238 bnj580 33299 bnj864 33308 bnj865 33309 bnj1049 33360 bnj1090 33365 bnj1093 33366 bnj1133 33375 bnj1171 33386 climuzcnv 34035 axextprim 34048 biimpexp 34064 dfon2lem8 34156 frpoins3xpg 34176 frpoins3xp3g 34177 xpord2ind 34183 xpord3ind 34189 dffun10 34395 filnetlem4 34749 bj-substax12 35082 wl-2sb6d 35909 poimirlem25 35999 poimirlem30 36004 ralin 36602 r2alan 36603 inxpss 36668 moantr 36721 isat3 37665 isltrn2N 38479 cdlemefrs29bpre0 38755 cdleme32fva 38796 sn-axrep5v 40533 dford4 41219 fnwe2lem2 41244 isdomn3 41397 ifpidg 41526 ifpim23g 41530 elmapintrab 41611 undmrnresiss 41639 df3or2 41803 df3an2 41804 dfhe3 41810 dffrege76 41974 dffrege115 42013 ntrneiiso 42128 ismnushort 42346 pm11.62 42439 2sbc6g 42460 expcomdg 42547 impexpd 42560 dfvd2 42626 dfvd3 42638 rabssf 43094 2rexsb 45083 2rexrsb 45084 snlindsntor 46302 elbigo2 46388 exp12bd 46631 ralbidb 46635 ralbidc 46636 |
Copyright terms: Public domain | W3C validator |