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 267 | 1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: bi2bian9 915 xorbi12d 1470 sb8eu 2491 cleqh 2711 vtoclb 3236 vtoclbg 3240 ceqsexg 3304 elabgf 3317 reu6 3362 ru 3401 sbcbig 3447 unineq 3836 sbcnestgf 3947 preq12bg 4326 prel12g 4327 axrep1 4700 axrep4 4703 nalset 4723 opthg 4872 opelopabsb 4910 isso2i 4991 opeliunxp2 5182 resieq 5327 elimasng 5410 cbviota 5773 iota2df 5792 fnbrfvb 6146 fvelimab 6163 fvopab5 6217 fmptco 6303 fsng 6310 fsn2g 6311 fressnfv 6332 fnpr2g 6379 isorel 6476 isocnv 6480 isocnv3 6482 isotr 6486 ovg 6697 caovcang 6733 caovordg 6739 caovord3d 6742 caovord 6743 orduninsuc 6935 opeliunxp2f 7223 brtpos 7248 dftpos4 7258 omopth 7625 ecopovsym 7736 xpf1o 8007 nneneq 8028 r1pwALT 8592 karden 8641 infxpenlem 8719 aceq0 8824 cflim2 8968 zfac 9165 ttukeylem1 9214 axextnd 9292 axrepndlem1 9293 axrepndlem2 9294 axrepnd 9295 axacndlem5 9312 zfcndrep 9315 zfcndac 9320 winalim 9396 gruina 9519 ltrnq 9680 ltsosr 9794 ltasr 9800 axpre-lttri 9865 axpre-ltadd 9867 nn0sub 11220 zextle 11326 zextlt 11327 xlesubadd 11965 sqeqor 12840 nn0opth2 12921 rexfiuz 13935 climshft 14155 rpnnen2lem10 14791 dvdsext 14881 ltoddhalfle 14923 halfleoddlt 14924 sumodd 14949 sadcadd 15018 dvdssq 15118 isprm2lem 15232 rpexp 15270 pcdvdsb 15411 imasleval 16024 isacs2 16137 acsfiel 16138 funcres2b 16380 pospropd 16957 isnsg 17446 nsgbi 17448 elnmz 17456 nmzbi 17457 oddvdsnn0 17786 odeq 17792 odmulg 17796 isslw 17846 slwispgp 17849 gsumval3lem2 18130 gsumcom2 18197 abveq0 18649 cnt0 20960 kqfvima 21343 kqt0lem 21349 isr0 21350 r0cld 21351 regr1lem2 21353 nrmr0reg 21362 isfildlem 21471 cnextfvval 21679 xmeteq0 21953 imasf1oxmet 21990 comet 22128 dscmet 22187 nrmmetd 22189 tngngp 22268 tngngp3 22270 mbfsup 23237 mbfinf 23238 degltlem1 23636 logltb 24150 cxple2 24243 rlimcnp 24492 rlimcnp2 24493 isppw2 24641 sqf11 24665 f1otrgitv 25550 isrgrac 26461 eupath2lem3 26506 nmlno0i 27033 nmlno0 27034 blocn 27046 ubth 27113 hvsubeq0 27309 hvaddcan 27311 hvsubadd 27318 normsub0 27377 hlim2 27433 pjoc1 27677 pjoc2 27682 chne0 27737 chsscon3 27743 chlejb1 27755 chnle 27757 h1de2ci 27799 elspansn 27809 elspansn2 27810 cmbr3 27851 cmcm 27857 cmcm3 27858 pjch1 27913 pjch 27937 pj11 27957 pjnel 27969 eigorth 28081 elnlfn 28171 nmlnop0 28241 lnopeq 28252 lnopcon 28278 lnfncon 28299 pjdifnormi 28410 chrelat2 28613 cvexch 28617 mdsym 28655 fmptcof2 28839 signswch 29964 cvmlift2lem12 30550 cvmlift2lem13 30551 abs2sqle 30828 abs2sqlt 30829 dfpo2 30898 br1steqg 30919 br2ndeqg 30920 axextdist 30949 brimageg 31204 brdomaing 31212 brrangeg 31213 elhf2 31452 nn0prpwlem 31487 nn0prpw 31488 onsuct0 31610 bj-abbi 31963 bj-axrep1 31976 bj-axrep4 31979 bj-nalset 31982 bj-sbceqgALT 32089 bj-ru0 32124 matunitlindf 32577 prdsbnd2 32764 isdrngo1 32925 lsatcmp 33308 llnexchb2 34173 lautset 34386 lautle 34388 zindbi 36529 wepwsolem 36630 aomclem8 36649 ntrneik13 37416 ntrneix13 37417 ntrneik4w 37418 2sbc6g 37638 2sbc5g 37639 dfcleqf 38281 wessf1ornlem 38366 fourierdlem31 39031 fourierdlem42 39042 fourierdlem54 39053 nbuhgr2vtx1edgb 40574 dfconngr1 41355 eupth2lem3lem6 41401 |
Copyright terms: Public domain | W3C validator |