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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  wdomtr  9334  ltaddsub  11449  leaddsub  11451  eqneg  11695  sqreulem  15071  brcic  17510  nmzsubg  18793  f1omvdconj  19054  dfod2  19171  odf1o2  19178  cyggenod  19484  lvecvscan  20373  znidomb  20769  mdetunilem9  21769  iccpnfcnv  24107  dvcvx  25184  cxple2  25852  wilthlem1  26217  lgslem1  26445  colinearalglem2  27275  axeuclidlem  27330  axcontlem7  27338  fusgrfisstep  27696  hvmulcan  29434  unopf1o  30278  ballotlemrv  32486  subfacp1lem3  33144  subfacp1lem5  33146  wl-sbcom2d  35716  poimirlem26  35803  areacirclem1  35865  areacirc  35870  cdleme50eq  38555  hdmapeq0  39858  hdmap11  39862  rmxdiophlem  40837  nnsum3primesle9  45246  0ringdif  45428