Theorem 3bitr3rd 313

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr3d.2	⊢ (𝜑 → (𝜓 ↔ 𝜃))
3bitr3d.3	⊢ (𝜑 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
3bitr3rd	⊢ (𝜑 → (𝜏 ↔ 𝜃))

Proof of Theorem 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 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

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  9023  ltaddsub  11103  leaddsub  11105  eqneg  11349  sqreulem  14711  brcic  17060  nmzsubg  18309  f1omvdconj  18566  dfod2  18683  odf1o2  18690  cyggenod  18996  lvecvscan  19876  znidomb  20253  mdetunilem9  21225  iccpnfcnv  23549  dvcvx  24623  cxple2  25288  wilthlem1  25653  lgslem1  25881  colinearalglem2  26701  axeuclidlem  26756  axcontlem7  26764  fusgrfisstep  27119  hvmulcan  28855  unopf1o  29699  ballotlemrv  31887  subfacp1lem3  32542  subfacp1lem5  32544  wl-sbcom2d  34962  poimirlem26  35083  areacirclem1  35145  areacirc  35150  cdleme50eq  37837  hdmapeq0  39140  hdmap11  39144  rmxdiophlem  39956  nnsum3primesle9  44312  0ringdif  44494