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  9553  ltaddsub  11771  leaddsub  11773  eqneg  12018  sqreulem  15507  brcic  17953  nmzsubg  19355  f1omvdconj  19640  dfod2  19758  odf1o2  19767  cyggenod  20078  0ringdif  20758  lvecvscan  21369  znidomb  21847  mdetunilem9  22915  iccpnfcnv  25245  dvcvx  26320  cxple2  27007  wilthlem1  27377  lgslem1  27606  eucliddivs  28744  colinearalglem2  29467  axeuclidlem  29522  axcontlem7  29530  fusgrfisstep  29892  hvmulcan  31656  unopf1o  32500  ballotlemrv  35135  subfacp1lem3  35916  subfacp1lem5  35918  wl-sbcom2d  38461  poimirlem26  38532  areacirclem1  38594  areacirc  38599  cdleme50eq  41566  hdmapeq0  42869  hdmap11  42873  ef11d  43358  rmxdiophlem  43975  ordeldif1o  44220  ceilbi  48351  nnsum3primesle9  48836