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  9483  ltaddsub  11615  leaddsub  11617  eqneg  11866  sqreulem  15313  brcic  17756  nmzsubg  19131  f1omvdconj  19412  dfod2  19530  odf1o2  19539  cyggenod  19850  0ringdif  20495  lvecvscan  21101  znidomb  21551  mdetunilem9  22595  iccpnfcnv  24921  dvcvx  25997  cxple2  26674  wilthlem1  27045  lgslem1  27274  eucliddivs  28382  colinearalglem2  28990  axeuclidlem  29045  axcontlem7  29053  fusgrfisstep  29412  hvmulcan  31158  unopf1o  32002  ballotlemrv  34680  subfacp1lem3  35380  subfacp1lem5  35382  wl-sbcom2d  37900  poimirlem26  37981  areacirclem1  38043  areacirc  38048  cdleme50eq  41001  hdmapeq0  42304  hdmap11  42308  ef11d  42785  rmxdiophlem  43461  ordeldif1o  43706  ceilbi  47797  nnsum3primesle9  48282