![]() |
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 281 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
5 | 1, 4 | bitr3d 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: wdomtr 9576 ltaddsub 11695 leaddsub 11697 eqneg 11941 sqreulem 15313 brcic 17752 nmzsubg 19088 f1omvdconj 19362 dfod2 19480 odf1o2 19489 cyggenod 19800 0ringdif 20423 lvecvscan 20957 znidomb 21426 mdetunilem9 22441 iccpnfcnv 24788 dvcvx 25872 cxple2 26544 wilthlem1 26912 lgslem1 27142 colinearalglem2 28597 axeuclidlem 28652 axcontlem7 28660 fusgrfisstep 29018 hvmulcan 30757 unopf1o 31601 ballotlemrv 33981 subfacp1lem3 34636 subfacp1lem5 34638 wl-sbcom2d 36889 poimirlem26 36977 areacirclem1 37039 areacirc 37044 cdleme50eq 39875 hdmapeq0 41178 hdmap11 41182 rmxdiophlem 42216 ordeldif1o 42472 nnsum3primesle9 46920 |
Copyright terms: Public domain | W3C validator |