Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitr3rd | Structured version Visualization version GIF version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr3d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr3d.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
3bitr3d.3 | ⊢ (𝜑 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
3bitr3rd | ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3d.3 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏)) | |
2 | 3bitr3d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 3bitr3d.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | bitr3d 280 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
5 | 1, 4 | bitr3d 280 | 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: wdomtr 9334 ltaddsub 11449 leaddsub 11451 eqneg 11695 sqreulem 15071 brcic 17510 nmzsubg 18793 f1omvdconj 19054 dfod2 19171 odf1o2 19178 cyggenod 19484 lvecvscan 20373 znidomb 20769 mdetunilem9 21769 iccpnfcnv 24107 dvcvx 25184 cxple2 25852 wilthlem1 26217 lgslem1 26445 colinearalglem2 27275 axeuclidlem 27330 axcontlem7 27338 fusgrfisstep 27696 hvmulcan 29434 unopf1o 30278 ballotlemrv 32486 subfacp1lem3 33144 subfacp1lem5 33146 wl-sbcom2d 35716 poimirlem26 35803 areacirclem1 35865 areacirc 35870 cdleme50eq 38555 hdmapeq0 39858 hdmap11 39862 rmxdiophlem 40837 nnsum3primesle9 45246 0ringdif 45428 |
Copyright terms: Public domain | W3C validator |