![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bibi12d | Structured version Visualization version GIF 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 332 | . 2 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
3 | imbi12d.2 | . . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 3 | bibi2d 331 | . 2 ⊢ (𝜑 → ((𝜒 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
5 | 2, 4 | bitrd 268 | 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: bi2bian9 937 xorbi12d 1518 sb8eu 2532 cleqh 2753 vtoclb 3294 vtoclbg 3298 ceqsexg 3365 elabgf 3380 reu6 3428 ru 3467 sbcbig 3513 unineq 3910 sbcnestgf 4028 preq12bg 4417 prel12g 4418 axrep1 4805 axrep4 4808 nalset 4828 opthg 4975 opelopabsb 5014 isso2i 5096 opeliunxp2 5293 resieq 5442 elimasng 5526 cbviota 5894 iota2df 5913 fnbrfvb 6274 fvelimab 6292 fvopab5 6349 fmptco 6436 fsng 6444 fsn2g 6445 fressnfv 6467 fnpr2g 6515 isorel 6616 isocnv 6620 isocnv3 6622 isotr 6626 ovg 6841 caovcang 6877 caovordg 6883 caovord3d 6886 caovord 6887 orduninsuc 7085 opeliunxp2f 7381 brtpos 7406 dftpos4 7416 omopth 7783 ecopovsym 7892 xpf1o 8163 nneneq 8184 r1pwALT 8747 karden 8796 infxpenlem 8874 aceq0 8979 cflim2 9123 zfac 9320 ttukeylem1 9369 axextnd 9451 axrepndlem1 9452 axrepndlem2 9453 axrepnd 9454 axacndlem5 9471 zfcndrep 9474 zfcndac 9479 winalim 9555 gruina 9678 ltrnq 9839 ltsosr 9953 ltasr 9959 axpre-lttri 10024 axpre-ltadd 10026 nn0sub 11381 zextle 11488 zextlt 11489 xlesubadd 12131 sqeqor 13018 nn0opth2 13099 rexfiuz 14131 climshft 14351 rpnnen2lem10 14996 dvdsext 15090 ltoddhalfle 15132 halfleoddlt 15133 sumodd 15158 sadcadd 15227 dvdssq 15327 rpexp 15479 pcdvdsb 15620 imasleval 16248 isacs2 16361 acsfiel 16362 funcres2b 16604 pospropd 17181 isnsg 17670 nsgbi 17672 elnmz 17680 nmzbi 17681 oddvdsnn0 18009 odeq 18015 odmulg 18019 isslw 18069 slwispgp 18072 gsumval3lem2 18353 gsumcom2 18420 abveq0 18874 cnt0 21198 kqfvima 21581 kqt0lem 21587 isr0 21588 r0cld 21589 regr1lem2 21591 nrmr0reg 21600 isfildlem 21708 cnextfvval 21916 xmeteq0 22190 imasf1oxmet 22227 comet 22365 dscmet 22424 nrmmetd 22426 tngngp 22505 tngngp3 22507 mbfsup 23476 mbfinf 23477 degltlem1 23877 logltb 24391 cxple2 24488 rlimcnp 24737 rlimcnp2 24738 isppw2 24886 sqf11 24910 f1otrgitv 25795 nbuhgr2vtx1edgb 26293 dfconngr1 27166 eupth2lem3lem6 27211 nmlno0i 27777 nmlno0 27778 blocn 27790 ubth 27857 hvsubeq0 28053 hvaddcan 28055 hvsubadd 28062 normsub0 28121 hlim2 28177 pjoc1 28421 pjoc2 28426 chne0 28481 chsscon3 28487 chlejb1 28499 chnle 28501 h1de2ci 28543 elspansn 28553 elspansn2 28554 cmbr3 28595 cmcm 28601 cmcm3 28602 pjch1 28657 pjch 28681 pj11 28701 pjnel 28713 eigorth 28825 elnlfn 28915 nmlnop0 28985 lnopeq 28996 lnopcon 29022 lnfncon 29043 pjdifnormi 29154 chrelat2 29357 cvexch 29361 mdsym 29399 fmptcof2 29585 signswch 30766 cvmlift2lem12 31422 cvmlift2lem13 31423 abs2sqle 31700 abs2sqlt 31701 dfpo2 31771 eqfunresadj 31785 br1steqgOLD 31798 br2ndeqgOLD 31799 axextdist 31829 slerec 32048 brimageg 32159 brdomaing 32167 brrangeg 32168 elhf2 32407 nn0prpwlem 32442 nn0prpw 32443 onsuct0 32565 bj-abbi 32900 bj-axrep1 32913 bj-axrep4 32916 bj-nalset 32919 bj-sbceqgALT 33022 bj-ru0 33057 dfgcd3 33300 matunitlindf 33537 prdsbnd2 33724 isdrngo1 33885 eqrelf 34161 elsymrels5 34442 lsatcmp 34608 llnexchb2 35473 lautset 35686 lautle 35688 zindbi 37828 wepwsolem 37929 aomclem8 37948 ntrneik13 38713 ntrneix13 38714 ntrneik4w 38715 2sbc6g 38933 2sbc5g 38934 wessf1ornlem 39685 fourierdlem31 40673 fourierdlem42 40684 fourierdlem54 40695 sprsymrelf 42070 sprsymrelfo 42072 |
Copyright terms: Public domain | W3C validator |