Theorem 3bitr3rd 309

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  9598  ltaddsub  11718  leaddsub  11720  eqneg  11964  sqreulem  15338  brcic  17780  nmzsubg  19124  f1omvdconj  19405  dfod2  19523  odf1o2  19532  cyggenod  19843  0ringdif  20468  lvecvscan  21003  znidomb  21499  mdetunilem9  22552  iccpnfcnv  24899  dvcvx  25983  cxple2  26661  wilthlem1  27030  lgslem1  27260  colinearalglem2  28774  axeuclidlem  28829  axcontlem7  28837  fusgrfisstep  29198  hvmulcan  30938  unopf1o  31782  ballotlemrv  34209  subfacp1lem3  34862  subfacp1lem5  34864  wl-sbcom2d  37098  poimirlem26  37189  areacirclem1  37251  areacirc  37256  cdleme50eq  40083  hdmapeq0  41386  hdmap11  41390  ef11d  41975  rmxdiophlem  42501  ordeldif1o  42754  nnsum3primesle9  47197