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  9551  ltaddsub  11716  leaddsub  11718  eqneg  11963  sqreulem  15451  brcic  17893  nmzsubg  19294  f1omvdconj  19579  dfod2  19697  odf1o2  19706  cyggenod  20017  0ringdif  20694  lvecvscan  21304  znidomb  21780  mdetunilem9  22848  iccpnfcnv  25178  dvcvx  26254  cxple2  26942  wilthlem1  27312  lgslem1  27541  eucliddivs  28649  colinearalglem2  29372  axeuclidlem  29427  axcontlem7  29435  fusgrfisstep  29797  hvmulcan  31561  unopf1o  32405  ballotlemrv  35039  subfacp1lem3  35769  subfacp1lem5  35771  wl-sbcom2d  38332  poimirlem26  38403  areacirclem1  38465  areacirc  38470  cdleme50eq  41422  hdmapeq0  42725  hdmap11  42729  ef11d  43222  rmxdiophlem  43864  ordeldif1o  44109  ceilbi  48233  nnsum3primesle9  48718