Theorem 3bitr3rd 310

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 281	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
5	1, 4	bitr3d 281	1 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

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  9613  ltaddsub  11735  leaddsub  11737  eqneg  11985  sqreulem  15395  brcic  17846  nmzsubg  19196  f1omvdconj  19479  dfod2  19597  odf1o2  19606  cyggenod  19917  0ringdif  20544  lvecvscan  21131  znidomb  21598  mdetunilem9  22642  iccpnfcnv  24989  dvcvx  26074  cxple2  26754  wilthlem1  27126  lgslem1  27356  colinearalglem2  28937  axeuclidlem  28992  axcontlem7  29000  fusgrfisstep  29361  hvmulcan  31101  unopf1o  31945  ballotlemrv  34501  subfacp1lem3  35167  subfacp1lem5  35169  wl-sbcom2d  37542  poimirlem26  37633  areacirclem1  37695  areacirc  37700  cdleme50eq  40524  hdmapeq0  41827  hdmap11  41831  ef11d  42354  rmxdiophlem  43004  ordeldif1o  43250  nnsum3primesle9  47719