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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  wdomtr  9572  ltaddsub  11793  leaddsub  11795  eqneg  12040  sqreulem  15532  brcic  17978  nmzsubg  19380  f1omvdconj  19665  dfod2  19783  odf1o2  19792  cyggenod  20103  0ringdif  20783  lvecvscan  21394  znidomb  21872  mdetunilem9  22940  iccpnfcnv  25270  dvcvx  26345  cxple2  27030  wilthlem1  27400  lgslem1  27629  eucliddivs  28767  colinearalglem2  29490  axeuclidlem  29545  axcontlem7  29553  fusgrfisstep  29915  hvmulcan  31679  unopf1o  32523  ballotlemrv  35198  subfacp1lem3  36033  subfacp1lem5  36035  wl-sbcom2d  38586  poimirlem26  38657  areacirclem1  38719  areacirc  38724  cdleme50eq  41691  hdmapeq0  42994  hdmap11  42998  ef11d  43483  rmxdiophlem  44115  ordeldif1o  44355  ceilbi  48500  nnsum3primesle9  48985