![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imbi2i | Structured version Visualization version Unicode version |
Description: Introduce an antecedent to both sides of a logical equivalence. This and the next three rules are useful for building up wff's around a definition, in order to make use of the definition. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.) |
Ref | Expression |
---|---|
imbi2i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imbi2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi2i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | pm5.74i 249 |
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 189 |
This theorem is referenced by: iman 426 pm4.14 582 nan 584 pm5.32 642 anidmdbi 652 imimorb 888 pm5.6 923 nannan 1389 alimex 1703 19.36v 1820 19.36 2044 sblim 2226 sban 2228 sbhb 2267 2sb6 2273 mo2v 2306 moabs 2330 eu1 2339 r2allem 2763 r2alfOLD 2765 r3al 2768 r19.21t 2785 r19.21tOLD 2786 r19.21v 2793 ralbii 2819 r19.35 2937 reu2 3226 reu8 3234 2reu5lem3 3247 ssconb 3566 ssin 3654 difin 3680 reldisj 3808 ssundif 3851 raldifsni 4102 pwpw0 4120 pwsnALT 4193 unissb 4229 moabex 4659 dffr2 4799 dfepfr 4819 ssrel 4923 ssrel2 4925 dffr3 5201 dffr4 5396 fncnv 5647 fun11 5648 dff13 6159 marypha2lem3 7951 dfsup2 7958 wemapsolem 8065 inf2 8128 axinf2 8145 aceq1 8548 aceq0 8549 kmlem14 8593 dfackm 8596 zfac 8890 ac6n 8915 zfcndrep 9039 zfcndac 9044 axgroth6 9253 axgroth4 9257 grothprim 9259 prime 11016 raluz2 11208 fsuppmapnn0ub 12207 mptnn0fsuppr 12211 brtrclfv 13066 rpnnen2 14278 isprm2 14632 isprm4 14634 pgpfac1 17713 pgpfac 17717 isirred2 17929 pmatcollpw2lem 19801 isclo2 20104 lmres 20316 ist1-2 20363 is1stc2 20457 alexsubALTlem3 21064 itg2cn 22721 ellimc3 22834 plydivex 23250 vieta1 23265 dchrelbas2 24165 nmobndseqi 26420 nmobndseqiALT 26421 cvnbtwn3 27941 elat2 27993 ssrelf 28221 funcnvmptOLD 28270 isarchi2 28502 archiabl 28515 esumcvgre 28912 signstfvneq0 29461 bnj1098 29595 bnj1533 29663 bnj121 29681 bnj124 29682 bnj130 29685 bnj153 29691 bnj207 29692 bnj611 29729 bnj864 29733 bnj865 29734 bnj1000 29752 bnj978 29760 bnj1021 29775 bnj1047 29782 bnj1049 29783 bnj1090 29788 bnj1110 29791 bnj1128 29799 bnj1145 29802 bnj1171 29809 bnj1172 29810 bnj1174 29812 bnj1176 29814 bnj1280 29829 axinfprim 30333 dfon2lem9 30437 dffun10 30681 elicc3 30973 filnetlem4 31037 df3nandALT1 31057 df3nandALT2 31058 bj-ssbeq 31240 bj-ssb0 31241 bj-ax12ssb 31248 bj-ssbn 31254 bj-sbnf 31441 wl-nannan 31853 poimirlem30 31970 lcvnbtwn3 32594 isat3 32873 cdleme25cv 33925 cdlemefrs29bpre0 33963 cdlemk35 34479 dford4 35884 ifpidg 36135 ifpid1g 36138 ifpim23g 36139 ifpororb 36149 ifpbibib 36154 elinintrab 36183 undmrnresiss 36210 cotrintab 36221 elintima 36245 frege60b 36501 frege91 36550 frege97 36556 frege98 36557 dffrege99 36558 frege109 36568 frege110 36569 frege131 36590 frege133 36592 int-rightdistd 36627 int-sqdefd 36628 int-sqgeq0d 36633 pm10.541 36716 pm13.196a 36765 2sbc6g 36766 expcomdg 36856 impexpd 36870 jcn 37368 fsummulc1f 37647 fsumiunss 37654 dvmptmulf 37812 dvmptfprodlem 37819 sge0ltfirpmpt2 38268 hoidmv1le 38416 hoidmvle 38422 rmoanim 38600 ldepslinc 40355 sbidd-misc 40492 |
Copyright terms: Public domain | W3C validator |