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 269 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
5 | 1, 4 | bitr3d 269 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: wdomtr 8363 ltaddsub 10381 leaddsub 10383 eqneg 10624 sqreulem 13947 brcic 16281 nmzsubg 17458 f1omvdconj 17689 dfod2 17804 odf1o2 17811 cyggenod 18109 lvecvscan 18932 znidomb 19729 mdetunilem9 20245 iccpnfcnv 22551 dvcvx 23587 cxple2 24243 wilthlem1 24594 lgslem1 24822 colinearalglem2 25587 axeuclidlem 25642 axcontlem7 25650 hvmulcan 27313 unopf1o 28159 ballotlemrv 29908 subfacp1lem3 30418 subfacp1lem5 30420 wl-sbcom2d 32523 poimirlem26 32605 areacirclem1 32670 areacirc 32675 cdleme50eq 34847 hdmapeq0 36154 hdmap11 36158 rmxdiophlem 36600 nnsum3primesle9 40210 fusgrfisstep 40548 0ringdif 41660 |
Copyright terms: Public domain | W3C validator |