| 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 206 |
| 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 207 |
| This theorem is referenced by: snssgOLD 4784 inimasn 6176 isof1oidb 7344 oacan 8586 ecdmn0 8794 wemapwe 9737 ttrclselem2 9766 r1pw 9885 adderpqlem 10994 mulerpqlem 10995 lterpq 11010 ltanq 11011 genpass 11049 readdcan 11435 lemuldiv 12148 msq11 12169 avglt2 12505 qbtwnre 13241 iooshf 13466 clim2c 15541 lo1o1 15568 climabs0 15621 reef11 16155 absefib 16234 efieq1re 16235 nndivides 16300 oddnn02np1 16385 oddge22np1 16386 evennn02n 16387 evennn2n 16388 halfleoddlt 16399 pc2dvds 16917 pcmpt 16930 subsubc 17898 ghmqusker 19305 odmulgid 19572 gexdvds 19602 submcmn2 19857 obslbs 21750 cnntr 23283 cndis 23299 cnindis 23300 cnpdis 23301 lmres 23308 cmpfi 23416 ist0-4 23737 txhmeo 23811 tsmssubm 24151 blin 24431 cncfmet 24935 icopnfcnv 24973 lmmbrf 25296 iscauf 25314 causs 25332 mbfposr 25687 itg2gt0 25795 limcflf 25916 limcres 25921 lhop1 26053 dvdsr1p 26203 fsumvma2 27258 vmasum 27260 chpchtsum 27263 bposlem1 27328 addscan2 28026 slesubaddd 28123 mulscan2dlem 28204 iscgrgd 28521 tgcgr4 28539 lnrot1 28631 eqeelen 28919 nbusgreledg 29370 nb3grprlem2 29398 wspthsnwspthsnon 29936 rusgrnumwwlks 29994 clwwlkwwlksb 30073 clwwlknwwlksnb 30074 dmdmd 32319 nfpconfp 32642 funcnvmpt 32677 1stpreimas 32715 xrdifh 32782 swrdrn3 32940 lsmsnorb 33419 fldextrspunlsp 33724 rhmpreimacnlem 33883 ismntop 34027 eulerpartlemgh 34380 signslema 34577 fmlafvel 35390 topdifinfindis 37347 leceifl 37616 lindsadd 37620 lindsenlbs 37622 iblabsnclem 37690 ftc1anclem6 37705 areacirclem5 37719 areacirc 37720 brcoss3 38434 lsatfixedN 39010 cdlemg10c 40641 diaglbN 41057 dih1 41288 dihglbcpreN 41302 mapdcv 41662 dvdsexpnn0 42369 ef11d 42375 ellz1 42778 islssfg 43082 proot1ex 43208 tfsconcat00 43360 eliooshift 45519 clim2cf 45665 dfatdmfcoafv2 47266 sfprmdvdsmersenne 47590 odd2np1ALTV 47661 vopnbgrelself 47841 rrx2plordisom 48644 i0oii 48817 io1ii 48818 |
| Copyright terms: Public domain | W3C validator |