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 284 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
5 | 1, 4 | bitr3d 284 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: wdomtr 9112 ltaddsub 11192 leaddsub 11194 eqneg 11438 sqreulem 14809 brcic 17173 nmzsubg 18435 f1omvdconj 18692 dfod2 18809 odf1o2 18816 cyggenod 19122 lvecvscan 20002 znidomb 20380 mdetunilem9 21371 iccpnfcnv 23696 dvcvx 24772 cxple2 25440 wilthlem1 25805 lgslem1 26033 colinearalglem2 26853 axeuclidlem 26908 axcontlem7 26916 fusgrfisstep 27271 hvmulcan 29007 unopf1o 29851 ballotlemrv 32056 subfacp1lem3 32715 subfacp1lem5 32717 wl-sbcom2d 35339 poimirlem26 35426 areacirclem1 35488 areacirc 35493 cdleme50eq 38178 hdmapeq0 39481 hdmap11 39485 rmxdiophlem 40409 nnsum3primesle9 44780 0ringdif 44962 |
Copyright terms: Public domain | W3C validator |