![]() |
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 282 | . 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
4 | 3bitr4d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | |
5 | 3, 4 | bitr4d 282 | 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 4746 inimasn 6109 isof1oidb 7270 oacan 8496 ecdmn0 8696 wemapwe 9634 ttrclselem2 9663 r1pw 9782 adderpqlem 10891 mulerpqlem 10892 lterpq 10907 ltanq 10908 genpass 10946 readdcan 11330 lemuldiv 12036 msq11 12057 avglt2 12393 qbtwnre 13119 iooshf 13344 clim2c 15388 lo1o1 15415 climabs0 15468 reef11 16002 absefib 16081 efieq1re 16082 nndivides 16147 oddnn02np1 16231 oddge22np1 16232 evennn02n 16233 evennn2n 16234 halfleoddlt 16245 pc2dvds 16752 pcmpt 16765 subsubc 17740 odmulgid 19337 gexdvds 19367 submcmn2 19618 obslbs 21139 cnntr 22629 cndis 22645 cnindis 22646 cnpdis 22647 lmres 22654 cmpfi 22762 ist0-4 23083 txhmeo 23157 tsmssubm 23497 blin 23777 cncfmet 24275 icopnfcnv 24308 lmmbrf 24629 iscauf 24647 causs 24665 mbfposr 25019 itg2gt0 25128 limcflf 25248 limcres 25253 lhop1 25381 dvdsr1p 25529 fsumvma2 26565 vmasum 26567 chpchtsum 26570 bposlem1 26635 addscan2 27305 iscgrgd 27458 tgcgr4 27476 lnrot1 27568 eqeelen 27856 nbusgreledg 28304 nb3grprlem2 28332 wspthsnwspthsnon 28864 rusgrnumwwlks 28922 clwwlkwwlksb 29001 clwwlknwwlksnb 29002 dmdmd 31245 nfpconfp 31549 funcnvmpt 31586 1stpreimas 31622 xrdifh 31686 swrdrn3 31812 lsmsnorb 32175 ghmqusker 32201 rhmpreimacnlem 32468 ismntop 32610 eulerpartlemgh 32981 signslema 33177 fmlafvel 33982 topdifinfindis 35820 leceifl 36070 lindsadd 36074 lindsenlbs 36076 iblabsnclem 36144 ftc1anclem6 36159 areacirclem5 36173 areacirc 36174 brcoss3 36898 lsatfixedN 37474 cdlemg10c 39105 diaglbN 39521 dih1 39752 dihglbcpreN 39766 mapdcv 40126 dvdsexpnn0 40830 ellz1 41093 islssfg 41400 proot1ex 41531 eliooshift 43751 clim2cf 43898 dfatdmfcoafv2 45493 sfprmdvdsmersenne 45802 odd2np1ALTV 45873 rrx2plordisom 46816 i0oii 46959 io1ii 46960 |
Copyright terms: Public domain | W3C validator |