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 449 | . 2 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | |
2 | pm3.31 450 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒)) | |
3 | 1, 2 | impbii 210 | 1 ⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: imdistan 568 pm4.14 803 nan 825 pm4.87 837 pm5.6 995 2sb6 2085 r2allem 3200 r3al 3202 r19.23t 3313 ceqsralt 3529 rspc2gv 3631 ralrab 3684 ralrab2 3689 euind 3714 reu2 3715 reu3 3717 rmo4 3720 rmo3f 3724 reuind 3743 2reu5lem3 3747 rmo2 3869 rmo3 3871 rmo3OLD 3872 rmoanim 3877 rmoanimALT 3878 ralss 4036 rabss 4047 raldifb 4120 rabsssn 4599 raldifsni 4722 unissb 4863 elintrab 4881 ssintrab 4892 dftr5 5167 axrep5 5188 reusv2lem4 5293 reusv2 5295 reusv3 5297 raliunxp 5704 fununi 6423 fvn0ssdmfun 6835 dff13 7004 ordunisuc2 7547 dfom2 7570 dfsmo2 7975 qliftfun 8372 dfsup2 8897 wemapsolem 9003 iscard2 9394 acnnum 9467 aceq1 9532 dfac9 9551 dfacacn 9556 axgroth6 10239 sstskm 10253 infm3 11589 prime 12052 raluz 12285 raluz2 12286 nnwos 12304 ralrp 12399 facwordi 13639 cotr2g 14326 rexuzre 14702 limsupgle 14824 ello12 14863 elo12 14874 lo1resb 14911 rlimresb 14912 o1resb 14913 modfsummod 15139 isprm2 16016 isprm4 16018 isprm7 16042 acsfn2 16924 pgpfac1 19133 isirred2 19382 isdomn2 20002 coe1fzgsumd 20400 evl1gsumd 20450 islindf4 20912 ist1-2 21885 isnrm2 21896 dfconn2 21957 1stccn 22001 iskgen3 22087 hausdiag 22183 cnflf 22540 txflf 22544 cnfcf 22580 metcnp 23080 caucfil 23815 ovolgelb 24010 ismbl 24056 dyadmbllem 24129 itg2leub 24264 ellimc3 24406 mdegleb 24587 jensen 25494 dchrelbas2 25741 dchrelbas3 25742 nmoubi 28477 nmobndseqi 28484 nmobndseqiALT 28485 h1dei 29255 nmopub 29613 nmfnleub 29630 mdsl1i 30026 mdsl2i 30027 elat2 30045 moel 30180 islinds5 30860 eulerpartlemgvv 31534 bnj115 31895 bnj1109 31958 bnj1533 32024 bnj580 32085 bnj864 32094 bnj865 32095 bnj1049 32144 bnj1090 32149 bnj1093 32150 bnj1133 32159 bnj1171 32170 climuzcnv 32812 axextprim 32825 biimpexp 32844 dfpo2 32889 dfon2lem8 32933 dffun10 33273 filnetlem4 33627 wl-2sb6d 34676 wl-dfrmosb 34735 wl-dfrmov 34736 wl-dfrmof 34737 poimirlem25 34799 poimirlem30 34804 inxpss 35452 moantr 35499 isat3 36325 isltrn2N 37138 cdlemefrs29bpre0 37414 cdleme32fva 37455 sn-axrep5v 38988 dford4 39506 fnwe2lem2 39531 isdomn3 39684 ifpidg 39737 ifpim23g 39741 elmapintrab 39816 undmrnresiss 39844 df3or2 39993 df3an2 39994 dfhe3 40001 dffrege76 40165 dffrege115 40204 ntrneiiso 40321 pm11.62 40606 2sbc6g 40627 expcomdg 40714 impexpd 40727 dfvd2 40793 dfvd3 40805 rabssf 41266 2rexsb 43180 2rexrsb 43181 snlindsntor 44424 elbigo2 44510 |
Copyright terms: Public domain | W3C validator |