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 205

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 206

This theorem is referenced by:  wdomtr  9576  ltaddsub  11695  leaddsub  11697  eqneg  11941  sqreulem  15313  brcic  17752  nmzsubg  19088  f1omvdconj  19362  dfod2  19480  odf1o2  19489  cyggenod  19800  0ringdif  20423  lvecvscan  20957  znidomb  21426  mdetunilem9  22441  iccpnfcnv  24788  dvcvx  25872  cxple2  26544  wilthlem1  26912  lgslem1  27142  colinearalglem2  28597  axeuclidlem  28652  axcontlem7  28660  fusgrfisstep  29018  hvmulcan  30757  unopf1o  31601  ballotlemrv  33981  subfacp1lem3  34636  subfacp1lem5  34638  wl-sbcom2d  36889  poimirlem26  36977  areacirclem1  37039  areacirc  37044  cdleme50eq  39875  hdmapeq0  41178  hdmap11  41182  rmxdiophlem  42216  ordeldif1o  42472  nnsum3primesle9  46920