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 19788 isirred2 20053 isdomn2 20692 islindf4 21167 coe1fzgsumd 21595 evl1gsumd 21645 ist1-2 22620 isnrm2 22631 dfconn2 22692 1stccn 22736 iskgen3 22822 hausdiag 22918 cnflf 23275 txflf 23279 cnfcf 23315 metcnp 23819 caucfil 24569 ovolgelb 24766 ismbl 24812 dyadmbllem 24885 itg2leub 25021 ellimc3 25165 mdegleb 25351 jensen 26260 dchrelbas2 26507 dchrelbas3 26508 eqscut2 27067 nmoubi 29500 nmobndseqi 29507 nmobndseqiALT 29508 h1dei 30278 nmopub 30636 nmfnleub 30653 mdsl1i 31049 mdsl2i 31050 elat2 31068 islinds5 31937 eulerpartlemgvv 32737 bnj115 33098 bnj1109 33159 bnj1533 33225 bnj580 33286 bnj864 33295 bnj865 33296 bnj1049 33347 bnj1090 33352 bnj1093 33353 bnj1133 33362 bnj1171 33373 climuzcnv 34022 axextprim 34035 biimpexp 34051 dfon2lem8 34143 frpoins3xpg 34163 frpoins3xp3g 34164 xpord2ind 34170 xpord3ind 34176 dffun10 34385 filnetlem4 34739 bj-substax12 35072 wl-2sb6d 35899 poimirlem25 35989 poimirlem30 35994 ralin 36592 r2alan 36593 inxpss 36658 moantr 36711 isat3 37655 isltrn2N 38469 cdlemefrs29bpre0 38745 cdleme32fva 38786 sn-axrep5v 40523 dford4 41187 fnwe2lem2 41212 isdomn3 41365 ifpidg 41494 ifpim23g 41498 elmapintrab 41579 undmrnresiss 41607 df3or2 41771 df3an2 41772 dfhe3 41778 dffrege76 41942 dffrege115 41981 ntrneiiso 42096 ismnushort 42314 pm11.62 42407 2sbc6g 42428 expcomdg 42515 impexpd 42528 dfvd2 42594 dfvd3 42606 rabssf 43062 2rexsb 45051 2rexrsb 45052 snlindsntor 46270 elbigo2 46356 exp12bd 46599 ralbidb 46603 ralbidc 46604 |
Copyright terms: Public domain | W3C validator |