![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr4rd | Structured version Visualization version GIF version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr4d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr4d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
3bitr4d.3 | ⊢ (𝜑 → (𝜏 ↔ 𝜒)) |
Ref | Expression |
---|---|
3bitr4rd | ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4d.3 | . . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒)) | |
2 | 3bitr4d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | bitr4d 281 | . 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
4 | 3bitr4d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | |
5 | 3, 4 | bitr4d 281 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: snssgOLD 4793 inimasn 6167 isof1oidb 7336 oacan 8578 ecdmn0 8783 wemapwe 9740 ttrclselem2 9769 r1pw 9888 adderpqlem 10997 mulerpqlem 10998 lterpq 11013 ltanq 11014 genpass 11052 readdcan 11438 lemuldiv 12146 msq11 12167 avglt2 12503 qbtwnre 13232 iooshf 13457 clim2c 15507 lo1o1 15534 climabs0 15587 reef11 16121 absefib 16200 efieq1re 16201 nndivides 16266 oddnn02np1 16350 oddge22np1 16351 evennn02n 16352 evennn2n 16353 halfleoddlt 16364 pc2dvds 16881 pcmpt 16894 subsubc 17872 ghmqusker 19281 odmulgid 19552 gexdvds 19582 submcmn2 19837 obslbs 21728 cnntr 23270 cndis 23286 cnindis 23287 cnpdis 23288 lmres 23295 cmpfi 23403 ist0-4 23724 txhmeo 23798 tsmssubm 24138 blin 24418 cncfmet 24920 icopnfcnv 24958 lmmbrf 25281 iscauf 25299 causs 25317 mbfposr 25672 itg2gt0 25781 limcflf 25901 limcres 25906 lhop1 26038 dvdsr1p 26191 fsumvma2 27243 vmasum 27245 chpchtsum 27248 bposlem1 27313 addscan2 28007 slesubaddd 28100 mulscan2dlem 28179 iscgrgd 28440 tgcgr4 28458 lnrot1 28550 eqeelen 28838 nbusgreledg 29289 nb3grprlem2 29317 wspthsnwspthsnon 29850 rusgrnumwwlks 29908 clwwlkwwlksb 29987 clwwlknwwlksnb 29988 dmdmd 32233 nfpconfp 32549 funcnvmpt 32584 1stpreimas 32617 xrdifh 32682 swrdrn3 32819 lsmsnorb 33266 rhmpreimacnlem 33699 ismntop 33841 eulerpartlemgh 34212 signslema 34408 fmlafvel 35213 topdifinfindis 37053 leceifl 37310 lindsadd 37314 lindsenlbs 37316 iblabsnclem 37384 ftc1anclem6 37399 areacirclem5 37413 areacirc 37414 brcoss3 38131 lsatfixedN 38707 cdlemg10c 40338 diaglbN 40754 dih1 40985 dihglbcpreN 40999 mapdcv 41359 dvdsexpnn0 42129 ef11d 42135 ellz1 42424 islssfg 42731 proot1ex 42861 tfsconcat00 43013 eliooshift 45124 clim2cf 45271 dfatdmfcoafv2 46867 sfprmdvdsmersenne 47175 odd2np1ALTV 47246 vopnbgrelself 47422 rrx2plordisom 48111 i0oii 48253 io1ii 48254 |
Copyright terms: Public domain | W3C validator |