|   | 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 206 | 
| 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 207 | 
| This theorem is referenced by: wdomtr 9616 ltaddsub 11738 leaddsub 11740 eqneg 11988 sqreulem 15399 brcic 17843 nmzsubg 19184 f1omvdconj 19465 dfod2 19583 odf1o2 19592 cyggenod 19903 0ringdif 20528 lvecvscan 21114 znidomb 21581 mdetunilem9 22627 iccpnfcnv 24976 dvcvx 26060 cxple2 26740 wilthlem1 27112 lgslem1 27342 colinearalglem2 28923 axeuclidlem 28978 axcontlem7 28986 fusgrfisstep 29347 hvmulcan 31092 unopf1o 31936 ballotlemrv 34523 subfacp1lem3 35188 subfacp1lem5 35190 wl-sbcom2d 37563 poimirlem26 37654 areacirclem1 37716 areacirc 37721 cdleme50eq 40544 hdmapeq0 41847 hdmap11 41851 ef11d 42380 rmxdiophlem 43032 ordeldif1o 43278 nnsum3primesle9 47786 | 
| Copyright terms: Public domain | W3C validator |