![]() |
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 196 |
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 197 |
This theorem is referenced by: imor 427 ancomst 467 ifpn 1060 eximal 1856 19.43 1959 19.37v 2075 19.37 2247 dfsb3 2511 sbrim 2533 sbor 2535 mo4f 2654 2mos 2690 neor 3023 r3al 3078 r19.23t 3159 r19.23v 3161 r19.43 3231 ceqsralt 3369 ralab 3508 ralrab 3509 euind 3534 reu2 3535 rmo4 3540 reuind 3552 2reu5lem3 3556 rmo3 3669 dfdif3 3863 raldifb 3893 unss 3930 ralunb 3937 inssdif0 4090 dfnf5 4095 ssundif 4196 dfif2 4232 pwss 4319 ralsnsg 4360 disjsn 4390 snssg 4459 raldifsni 4470 raldifsnb 4471 unissb 4621 intun 4661 intpr 4662 dfiin2g 4705 disjor 4786 dftr2 4906 axrep1 4924 axpweq 4991 zfpow 4993 axpow2 4994 reusv2lem4 5021 reusv2 5023 raliunxp 5417 asymref2 5671 dffun2 6059 dffun4 6061 dffun5 6062 dffun7 6076 fununi 6125 fvn0ssdmfun 6514 dff13 6676 dff14b 6692 zfun 7116 uniex2 7118 dfom2 7233 fimaxg 8374 fiint 8404 dfsup2 8517 fiming 8571 oemapso 8754 scottexs 8925 scott0s 8926 iscard2 9012 acnnum 9085 dfac9 9170 dfacacn 9175 kmlem4 9187 kmlem12 9195 axpowndlem3 9633 zfcndun 9649 zfcndpow 9650 zfcndac 9653 axgroth5 9858 grothpw 9860 axgroth6 9862 addsrmo 10106 mulsrmo 10107 infm3 11194 raluz2 11950 nnwos 11968 ralrp 12065 cotr2g 13936 lo1resb 14514 rlimresb 14515 o1resb 14516 modfsummod 14745 isprm4 15619 acsfn1 16543 acsfn2 16545 lublecllem 17209 isirred2 18921 isdomn2 19521 iunocv 20247 ist1-2 21373 isnrm2 21384 dfconn2 21444 alexsubALTlem3 22074 ismbl 23514 dyadmbllem 23587 ellimc3 23862 dchrelbas2 25182 dchrelbas3 25183 isch2 28410 choc0 28515 h1dei 28739 mdsl2i 29511 rmo3f 29664 rmo4fOLD 29665 rmo4f 29666 disjorf 29720 bnj538OLD 31138 bnj1101 31183 bnj1109 31185 bnj1533 31250 bnj580 31311 bnj864 31320 bnj865 31321 bnj978 31347 bnj1049 31370 bnj1090 31375 bnj1145 31389 axextprim 31906 axunprim 31908 axpowprim 31909 untuni 31914 3orit 31924 biimpexp 31925 elintfv 31990 dfon2lem8 32021 soseq 32081 dfom5b 32346 bj-axrep1 33116 bj-zfpow 33123 bj-raldifsn 33378 rdgeqoa 33547 wl-equsalcom 33659 poimirlem25 33765 poimirlem30 33770 tsim1 34268 inxpss 34424 idinxpss 34425 idinxpssinxp 34429 ineleq 34460 cocossss 34532 cosscnvssid3 34567 trcoss2 34575 cvlsupr3 35152 pmapglbx 35576 isltrn2N 35927 cdlemefrs29bpre0 36204 fphpd 37900 dford4 38116 fnwe2lem2 38141 isdomn3 38302 ifpidg 38356 ifpid1g 38359 ifpor123g 38373 undmrnresiss 38430 elintima 38465 df3or2 38580 dfhe3 38589 dffrege76 38753 dffrege115 38792 frege131 38808 ntrneikb 38912 ntrneixb 38913 pm14.12 39142 dfvd2an 39318 dfvd3 39327 dfvd3an 39330 uun2221 39560 uun2221p1 39561 uun2221p2 39562 disjinfi 39897 supxrleubrnmptf 40196 fsummulc1f 40323 fsumiunss 40328 fnlimfvre2 40430 limsupreuz 40490 limsupvaluz2 40491 dvmptmulf 40673 dvnmul 40679 dvmptfprodlem 40680 dvnprodlem2 40683 sge0ltfirpmpt2 41164 hoidmv1le 41332 hoidmvle 41338 vonioolem2 41419 smflimlem3 41505 setrec2 42970 aacllem 43078 |
Copyright terms: Public domain | W3C validator |