![]() |
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 955 xorbi12d 1627 sb8eu 2641 cleqh 2862 vtoclb 3403 vtoclbg 3407 ceqsexg 3473 elabgf 3488 reu6 3536 ru 3575 sbcbig 3621 unineq 4020 sbcnestgf 4138 preq12bg 4530 prel12gOLD 4531 axrep1 4924 axrep4 4927 nalset 4947 opthg 5094 opelopabsb 5135 isso2i 5219 opeliunxp2 5416 resieq 5565 elimasng 5649 cbviota 6017 iota2df 6036 fnbrfvb 6398 fvelimab 6416 fvopab5 6473 fmptco 6560 fsng 6568 fsn2g 6569 fressnfv 6591 fnpr2g 6639 isorel 6740 isocnv 6744 isocnv3 6746 isotr 6750 ovg 6965 caovcang 7001 caovordg 7007 caovord3d 7010 caovord 7011 orduninsuc 7209 opeliunxp2f 7506 brtpos 7531 dftpos4 7541 omopth 7909 ecopovsym 8018 xpf1o 8289 nneneq 8310 r1pwALT 8884 karden 8933 infxpenlem 9046 aceq0 9151 cflim2 9297 zfac 9494 ttukeylem1 9543 axextnd 9625 axrepndlem1 9626 axrepndlem2 9627 axrepnd 9628 axacndlem5 9645 zfcndrep 9648 zfcndac 9653 winalim 9729 gruina 9852 ltrnq 10013 ltsosr 10127 ltasr 10133 axpre-lttri 10198 axpre-ltadd 10200 nn0sub 11555 zextle 11662 zextlt 11663 xlesubadd 12306 sqeqor 13192 nn0opth2 13273 rexfiuz 14306 climshft 14526 rpnnen2lem10 15171 dvdsext 15265 ltoddhalfle 15307 halfleoddlt 15308 sumodd 15333 sadcadd 15402 dvdssq 15502 rpexp 15654 pcdvdsb 15795 imasleval 16423 isacs2 16535 acsfiel 16536 funcres2b 16778 pospropd 17355 isnsg 17844 nsgbi 17846 elnmz 17854 nmzbi 17855 oddvdsnn0 18183 odeq 18189 odmulg 18193 isslw 18243 slwispgp 18246 gsumval3lem2 18527 gsumcom2 18594 abveq0 19048 cnt0 21372 kqfvima 21755 kqt0lem 21761 isr0 21762 r0cld 21763 regr1lem2 21765 nrmr0reg 21774 isfildlem 21882 cnextfvval 22090 xmeteq0 22364 imasf1oxmet 22401 comet 22539 dscmet 22598 nrmmetd 22600 tngngp 22679 tngngp3 22681 mbfsup 23650 mbfinf 23651 degltlem1 24051 logltb 24566 cxple2 24663 rlimcnp 24912 rlimcnp2 24913 isppw2 25061 sqf11 25085 f1otrgitv 25970 nbuhgr2vtx1edgb 26468 dfconngr1 27361 eupth2lem3lem6 27406 nmlno0i 27979 nmlno0 27980 blocn 27992 ubth 28059 hvsubeq0 28255 hvaddcan 28257 hvsubadd 28264 normsub0 28323 hlim2 28379 pjoc1 28623 pjoc2 28628 chne0 28683 chsscon3 28689 chlejb1 28701 chnle 28703 h1de2ci 28745 elspansn 28755 elspansn2 28756 cmbr3 28797 cmcm 28803 cmcm3 28804 pjch1 28859 pjch 28883 pj11 28903 pjnel 28915 eigorth 29027 elnlfn 29117 nmlnop0 29187 lnopeq 29198 lnopcon 29224 lnfncon 29245 pjdifnormi 29356 chrelat2 29559 cvexch 29563 mdsym 29601 fmptcof2 29787 signswch 30968 cvmlift2lem12 31624 cvmlift2lem13 31625 abs2sqle 31902 abs2sqlt 31903 dfpo2 31973 eqfunresadj 31987 br1steqgOLD 32000 br2ndeqgOLD 32001 axextdist 32031 slerec 32250 brimageg 32361 brdomaing 32369 brrangeg 32370 elhf2 32609 nn0prpwlem 32644 nn0prpw 32645 onsuct0 32767 bj-abbi 33103 bj-axrep1 33116 bj-axrep4 33119 bj-nalset 33122 bj-sbceqgALT 33219 bj-ru0 33257 dfgcd3 33499 matunitlindf 33738 prdsbnd2 33925 isdrngo1 34086 eqrelf 34362 elsymrels5 34643 lsatcmp 34811 llnexchb2 35676 lautset 35889 lautle 35891 zindbi 38031 wepwsolem 38132 aomclem8 38151 ntrneik13 38916 ntrneix13 38917 ntrneik4w 38918 2sbc6g 39136 2sbc5g 39137 wessf1ornlem 39888 fourierdlem31 40876 fourierdlem42 40887 fourierdlem54 40898 sprsymrelf 42273 sprsymrelfo 42275 |
Copyright terms: Public domain | W3C validator |