Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > imbi1i | Structured version Visualization version GIF version |
Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.) |
Ref | Expression |
---|---|
imbi1i.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
imbi1i | ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi1i.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
2 | imbi1 336 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 |
This theorem is referenced by: imor 427 ancomst 467 ifpn 1016 eximal 1698 19.43 1799 19.37v 1897 19.37 2087 dfsb3 2362 sbrim 2384 sbor 2386 mo4f 2504 2mos 2540 neor 2873 r3al 2924 r19.23t 3003 r19.23v 3005 r19.43 3074 ceqsralt 3202 ralab 3334 ralrab 3335 euind 3360 reu2 3361 rmo4 3366 reuind 3378 2reu5lem3 3382 rmo3 3494 raldifb 3712 unss 3749 ralunb 3756 inssdif0 3901 dfnf5 3906 ssundif 4004 dfif2 4038 pwss 4123 ralsnsg 4163 disjsn 4192 snss 4259 raldifsni 4265 raldifsnb 4266 unissb 4405 intun 4444 intpr 4445 dfiin2g 4489 disjor 4567 dftr2 4682 axrep1 4700 axpweq 4768 zfpow 4770 axpow2 4771 reusv2lem4 4798 reusv2 4800 raliunxp 5183 asymref2 5432 dffun2 5814 dffun4 5816 dffun5 5817 dffun7 5830 fununi 5878 fvn0ssdmfun 6258 dff13 6416 dff14b 6428 zfun 6848 uniex2 6850 dfom2 6959 fimaxg 8092 fiint 8122 dfsup2 8233 fiming 8287 oemapso 8462 scottexs 8633 scott0s 8634 iscard2 8685 acnnum 8758 dfac9 8841 dfacacn 8846 kmlem4 8858 kmlem12 8866 axpowndlem3 9300 zfcndun 9316 zfcndpow 9317 zfcndac 9320 axgroth5 9525 grothpw 9527 axgroth6 9529 addsrmo 9773 mulsrmo 9774 infm3 10861 raluz2 11613 nnwos 11631 ralrp 11728 cotr2g 13563 lo1resb 14143 rlimresb 14144 o1resb 14145 modfsummod 14367 isprm4 15235 acsfn1 16145 acsfn2 16147 lublecllem 16811 isirred2 18524 isdomn2 19120 iunocv 19844 ist1-2 20961 isnrm2 20972 dfcon2 21032 alexsubALTlem3 21663 ismbl 23101 dyadmbllem 23173 ellimc3 23449 dchrelbas2 24762 dchrelbas3 24763 isch2 27464 choc0 27569 h1dei 27793 mdsl2i 28565 rmo3f 28719 rmo4fOLD 28720 rmo4f 28721 disjorf 28774 bnj538OLD 30064 bnj1101 30109 bnj1109 30111 bnj1533 30176 bnj580 30237 bnj864 30246 bnj865 30247 bnj978 30273 bnj1049 30296 bnj1090 30301 bnj1145 30315 axextprim 30832 axunprim 30834 axpowprim 30835 untuni 30840 3orit 30851 biimpexp 30852 dfon2lem8 30939 soseq 30995 dfom5b 31189 bj-axrep1 31976 bj-zfpow 31983 rdgeqoa 32394 wl-equsalcom 32507 poimirlem25 32604 poimirlem30 32609 tsim1 33107 cvlsupr3 33649 pmapglbx 34073 isltrn2N 34424 cdlemefrs29bpre0 34702 fphpd 36398 dford4 36614 fnwe2lem2 36639 isdomn3 36801 ifpidg 36855 ifpid1g 36858 ifpor123g 36872 undmrnresiss 36929 elintima 36964 df3or2 37079 dfhe3 37089 dffrege76 37253 dffrege115 37292 frege131 37308 ntrneikb 37412 ntrneixb 37413 pm14.12 37644 dfvd2an 37819 dfvd3 37828 dfvd3an 37831 uun2221 38061 uun2221p1 38062 uun2221p2 38063 disjinfi 38375 fsummulc1f 38635 fsumiunss 38642 fnlimfvre2 38744 dvmptmulf 38827 dvnmul 38833 dvmptfprodlem 38834 dvnprodlem2 38837 sge0ltfirpmpt2 39319 hoidmv1le 39484 hoidmvle 39490 vonioolem2 39572 smflimlem3 39659 setrec2 42241 aacllem 42356 |
Copyright terms: Public domain | W3C validator |