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 459 | . 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | |
2 | pm3.31 460 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒)) | |
3 | 1, 2 | impbii 198 | 1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: pm4.14 600 nan 602 pm4.87 606 imp4aOLD 613 exp4aOLD 632 imdistan 721 pm5.3 744 pm5.6 949 2sb6 2432 r2allem 2921 r3al 2924 r19.23t 3003 ceqsralt 3202 ralrab 3335 ralrab2 3339 euind 3360 reu2 3361 reu3 3363 rmo4 3366 reuind 3378 2reu5lem3 3382 rmo2 3492 rmo3 3494 ralss 3631 rabss 3642 raldifb 3712 rabsssn 4162 raldifsni 4265 unissb 4405 elintrab 4423 ssintrab 4435 dftr5 4683 axrep5 4704 reusv2lem4 4798 reusv2 4800 reusv3 4802 raliunxp 5183 fununi 5878 fvn0ssdmfun 6258 dff13 6416 ordunisuc2 6936 dfom2 6959 dfsmo2 7331 qliftfun 7719 dfsup2 8233 wemapsolem 8338 iscard2 8685 acnnum 8758 aceq1 8823 dfac9 8841 dfacacn 8846 axgroth6 9529 sstskm 9543 infm3 10861 prime 11334 raluz 11612 raluz2 11613 nnwos 11631 ralrp 11728 facwordi 12938 cotr2g 13563 rexuzre 13940 limsupgle 14056 ello12 14095 elo12 14106 lo1resb 14143 rlimresb 14144 o1resb 14145 modfsummod 14367 isprm2 15233 isprm4 15235 isprm7 15258 acsfn2 16147 pgpfac1 18302 isirred2 18524 isdomn2 19120 coe1fzgsumd 19493 evl1gsumd 19542 islindf4 19996 ist1-2 20961 isnrm2 20972 dfcon2 21032 1stccn 21076 iskgen3 21162 hausdiag 21258 cnflf 21616 txflf 21620 cnfcf 21656 metcnp 22156 caucfil 22889 ovolgelb 23055 ismbl 23101 dyadmbllem 23173 itg2leub 23307 ellimc3 23449 mdegleb 23628 jensen 24515 dchrelbas2 24762 dchrelbas3 24763 nmoubi 27011 nmobndseqi 27018 nmobndseqiALT 27019 h1dei 27793 nmopub 28151 nmfnleub 28168 mdsl1i 28564 mdsl2i 28565 elat2 28583 moel 28707 rmo3f 28719 rmo4fOLD 28720 eulerpartlemgvv 29765 bnj115 30045 bnj1109 30111 bnj1533 30176 bnj580 30237 bnj864 30246 bnj865 30247 bnj1049 30296 bnj1090 30301 bnj1093 30302 bnj1133 30311 bnj1171 30322 climuzcnv 30819 axextprim 30832 biimpexp 30852 dfpo2 30898 dfon2lem8 30939 dffun10 31191 filnetlem4 31546 bj-axrep5 31980 wl-2sb6d 32520 poimirlem25 32604 poimirlem30 32609 isat3 33612 isltrn2N 34424 cdlemefrs29bpre0 34702 cdleme32fva 34743 dford4 36614 fnwe2lem2 36639 isdomn3 36801 ifpidg 36855 ifpim23g 36859 elmapintrab 36901 undmrnresiss 36929 df3or2 37079 df3an2 37080 dfhe3 37089 dffrege76 37253 dffrege115 37292 ntrneiiso 37409 pm11.62 37616 2sbc6g 37638 expcomdg 37727 impexpd 37740 dfvd2 37816 dfvd3 37828 rabssf 38334 2rexsb 39819 2rexrsb 39820 rmoanim 39828 snlindsntor 42054 elbigo2 42144 |
Copyright terms: Public domain | W3C validator |