![]() |
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 273 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
5 | 1, 4 | bitr3d 273 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: wdomtr 8720 ltaddsub 10792 leaddsub 10794 eqneg 11035 sqreulem 14437 brcic 16769 nmzsubg 17945 f1omvdconj 18175 dfod2 18291 odf1o2 18298 cyggenod 18598 lvecvscan 19429 znidomb 20228 mdetunilem9 20749 iccpnfcnv 23068 dvcvx 24121 cxple2 24781 wilthlem1 25143 lgslem1 25371 colinearalglem2 26136 axeuclidlem 26191 axcontlem7 26199 fusgrfisstep 26555 hvmulcan 28446 unopf1o 29292 ballotlemrv 31090 subfacp1lem3 31673 subfacp1lem5 31675 wl-sbcom2d 33826 poimirlem26 33916 areacirclem1 33980 areacirc 33985 cdleme50eq 36554 hdmapeq0 37857 hdmap11 37861 rmxdiophlem 38355 nnsum3primesle9 42452 0ringdif 42657 |
Copyright terms: Public domain | W3C validator |