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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  wdomtr  9471  ltaddsub  11601  leaddsub  11603  eqneg  11851  sqreulem  15277  brcic  17715  nmzsubg  19087  f1omvdconj  19368  dfod2  19486  odf1o2  19495  cyggenod  19806  0ringdif  20452  lvecvscan  21058  znidomb  21508  mdetunilem9  22545  iccpnfcnv  24879  dvcvx  25962  cxple2  26643  wilthlem1  27015  lgslem1  27245  eucliddivs  28311  colinearalglem2  28896  axeuclidlem  28951  axcontlem7  28959  fusgrfisstep  29318  hvmulcan  31063  unopf1o  31907  ballotlemrv  34544  subfacp1lem3  35237  subfacp1lem5  35239  wl-sbcom2d  37616  poimirlem26  37696  areacirclem1  37758  areacirc  37763  cdleme50eq  40650  hdmapeq0  41953  hdmap11  41957  ef11d  42447  rmxdiophlem  43122  ordeldif1o  43367  ceilbi  47447  nnsum3primesle9  47908