![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bibi12d | Structured version Visualization version Unicode version |
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
imbi12d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
imbi12d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bibi12d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi12d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bibi1d 325 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | imbi12d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | bibi2d 324 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 261 |
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: bi2bian9 891 xorbi12d 1432 sb8eu 2343 cleqh 2563 vtoclb 3116 vtoclbg 3120 ceqsexg 3182 elabgf 3195 reu6 3239 ru 3278 sbcbig 3324 unineq 3705 sbcnestgf 3796 preq12bg 4168 prel12g 4169 axrep1 4530 axrep4 4533 nalset 4554 opthg 4691 opelopabsb 4725 isso2i 4806 opeliunxp2 4992 resieq 5134 elimasng 5213 cbviota 5570 iota2df 5589 fnbrfvb 5928 fvelimab 5944 fvopab5 5997 fmptco 6080 fsng 6087 fsn2g 6088 fressnfv 6102 fnpr2g 6149 isorel 6242 isocnv 6246 isocnv3 6248 isotr 6252 ovg 6462 caovcang 6497 caovordg 6503 caovord3d 6506 caovord 6507 orduninsuc 6697 opeliunxp2f 6983 brtpos 7008 dftpos4 7018 omopth 7385 ecopovsym 7491 xpf1o 7760 nneneq 7781 r1pwALT 8343 karden 8392 infxpenlem 8470 aceq0 8575 cflim2 8719 zfac 8916 ttukeylem1 8965 axextnd 9042 axrepndlem1 9043 axrepndlem2 9044 axrepnd 9045 axacndlem5 9062 zfcndrep 9065 zfcndac 9070 winalim 9146 gruina 9269 ltrnq 9430 ltsosr 9544 ltasr 9550 axpre-lttri 9615 axpre-ltadd 9617 nn0sub 10949 zextle 11038 zextlt 11039 xlesubadd 11578 sqeqor 12420 nn0opth2 12490 rexfiuz 13459 climshft 13689 rpnnen2lem10 14325 dvdsext 14405 sadcadd 14481 dvdssq 14577 isprm2lem 14680 rpexp 14721 pcdvdsb 14867 imasleval 15496 isacs2 15608 acsfiel 15609 funcres2b 15851 pospropd 16429 isnsg 16895 nsgbi 16897 elnmz 16905 nmzbi 16906 oddvdsnn0 17242 odeq 17248 odmulg 17256 isslw 17309 slwispgp 17312 gsumval3lem2 17589 gsumcom2 17656 abveq0 18103 cnt0 20411 kqfvima 20794 kqt0lem 20800 isr0 20801 r0cld 20802 regr1lem2 20804 nrmr0reg 20813 isfildlem 20921 cnextfvval 21129 xmeteq0 21402 imasf1oxmet 21439 comet 21577 dscmet 21636 nrmmetd 21638 tngngp 21711 mbfsup 22669 mbfinf 22670 mbfinfOLD 22671 degltlem1 23070 logltb 23598 cxple2 23691 rlimcnp 23940 rlimcnp2 23941 isppw2 24091 sqf11 24115 f1otrgitv 24949 isrgrac 25711 eupath2lem3 25756 nmlno0i 26484 nmlno0 26485 blocn 26497 ubth 26564 hvsubeq0 26770 hvaddcan 26772 hvsubadd 26779 normsub0 26838 hlim2 26894 pjoc1 27136 pjoc2 27141 chne0 27196 chsscon3 27202 chlejb1 27214 chnle 27216 h1de2ci 27258 elspansn 27268 elspansn2 27269 cmbr3 27310 cmcm 27316 cmcm3 27317 pjch1 27372 pjch 27396 pj11 27416 pjnel 27428 eigorth 27540 elnlfn 27630 nmlnop0 27700 lnopeq 27711 lnopcon 27737 lnfncon 27758 pjdifnormi 27869 chrelat2 28072 cvexch 28076 mdsym 28114 fmptcof2 28308 signswch 29499 cvmlift2lem12 30086 cvmlift2lem13 30087 abs2sqle 30373 abs2sqlt 30374 dfpo2 30444 br1steqg 30465 br2ndeqg 30466 axextdist 30495 brimageg 30743 brdomaing 30751 brrangeg 30752 elhf2 30991 nn0prpwlem 31027 nn0prpw 31028 onsuct0 31150 bj-abbi 31435 bj-axrep1 31448 bj-axrep4 31451 bj-nalset 31454 bj-sbceqgALT 31549 bj-ru0 31582 prdsbnd2 32172 isdrngo1 32240 lsatcmp 32614 llnexchb2 33479 lautset 33692 lautle 33694 zindbi 35839 divalgmodcl 35887 wepwsolem 35945 aomclem8 35964 2sbc6g 36810 2sbc5g 36811 wessf1ornlem 37497 fourierdlem31 38038 fourierdlem31OLD 38039 fourierdlem42 38050 fourierdlem42OLD 38051 fourierdlem54 38062 nbuhgr2vtx1edgb 39470 dfconngr1 39929 |
Copyright terms: Public domain | W3C validator |