![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imbi1i | Structured version Visualization version Unicode 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 329 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 |
This theorem is referenced by: imor 418 ancomst 458 ifpn 1445 eximal 1676 19.43 1755 19.37v 1836 19.37 2056 dfsb3 2213 sbrim 2235 sbor 2237 mo4f 2355 2mos 2391 neor 2726 r3al 2779 r3alOLD 2837 r19.23t 2876 r19.23v 2878 r19.43 2957 ceqsralt 3082 ralab 3210 ralrab 3211 euind 3236 reu2 3237 rmo4 3242 reuind 3254 2reu5lem3 3258 rmo3 3369 raldifb 3584 unss 3619 ralunb 3626 inssdif0 3845 ssundif 3862 dfif2 3894 pwss 3977 ralsnsg 4014 disjsn 4043 snss 4108 raldifsni 4114 raldifsnb 4115 unissb 4242 intun 4280 intpr 4281 dfiin2g 4324 disjor 4400 dftr2 4512 axrep1 4529 axpweq 4593 zfpow 4595 axpow2 4596 reusv2lem4 4620 reusv2 4622 raliunxp 4992 asymref2 5235 dffun2 5610 dffun4 5612 dffun5 5613 dffun7 5626 fununi 5670 fvn0ssdmfun 6035 dff13 6183 dff14b 6195 zfun 6610 uniex2 6612 dfom2 6720 fimaxg 7843 fiint 7873 dfsup2 7983 fiming 8039 oemapso 8212 scottexs 8383 scott0s 8384 iscard2 8435 acnnum 8508 dfac9 8591 dfacacn 8596 kmlem4 8608 kmlem12 8616 axpowndlem3 9049 zfcndun 9065 zfcndpow 9066 zfcndac 9069 axgroth5 9274 grothpw 9276 axgroth6 9278 addsrmo 9522 mulsrmo 9523 infm3 10595 raluz2 11236 nnwos 11254 ralrp 11349 cotr2g 13088 lo1resb 13676 rlimresb 13677 o1resb 13678 modfsummod 13902 isprm4 14682 acsfn1 15615 acsfn2 15617 lublecllem 16282 isirred2 17977 isdomn2 18571 iunocv 19292 ist1-2 20411 isnrm2 20422 dfcon2 20482 alexsubALTlem3 21112 ismbl 22528 dyadmbllem 22605 ellimc3 22882 dchrelbas2 24213 dchrelbas3 24214 isch2 26924 choc0 27027 h1dei 27251 mdsl2i 28023 rmo3f 28179 rmo4fOLD 28180 rmo4f 28181 disjorf 28237 bnj538OLD 29598 bnj1101 29644 bnj1109 29646 bnj1533 29711 bnj580 29772 bnj864 29781 bnj865 29782 bnj978 29808 bnj1049 29831 bnj1090 29836 bnj1145 29850 axextprim 30376 axunprim 30378 axpowprim 30379 untuni 30384 3orit 30395 biimpexp 30396 dfon2lem8 30484 soseq 30540 dfom5b 30727 bj-axrep1 31447 bj-zfpow 31454 rdgeqoa 31817 wl-equsalcom 31919 poimirlem25 32009 poimirlem30 32014 tsim1 32416 cvlsupr3 32954 pmapglbx 33378 isltrn2N 33729 cdlemefrs29bpre0 34007 fphpd 35703 dford4 35928 fnwe2lem2 35953 isdomn3 36125 ifpidg 36179 ifpid1g 36182 ifpor123g 36196 undmrnresiss 36254 elintima 36289 df3or2 36404 dfhe3 36414 dffrege76 36579 dffrege115 36618 frege131 36634 pm14.12 36815 dfvd2an 36994 dfvd3 37003 dfvd3an 37006 uun2221 37239 uun2221p1 37240 uun2221p2 37241 disjinfi 37505 fsummulc1f 37684 fsumiunss 37691 dvmptmulf 37849 dvnmul 37855 dvmptfprodlem 37856 dvnprodlem2 37859 sge0ltfirpmpt2 38305 hoidmv1le 38453 hoidmvle 38459 aacllem 40812 |
Copyright terms: Public domain | W3C validator |