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  9492  ltaddsub  11623  leaddsub  11625  eqneg  11873  sqreulem  15295  brcic  17734  nmzsubg  19106  f1omvdconj  19387  dfod2  19505  odf1o2  19514  cyggenod  19825  0ringdif  20472  lvecvscan  21078  znidomb  21528  mdetunilem9  22576  iccpnfcnv  24910  dvcvx  25993  cxple2  26674  wilthlem1  27046  lgslem1  27276  eucliddivs  28384  colinearalglem2  28992  axeuclidlem  29047  axcontlem7  29055  fusgrfisstep  29414  hvmulcan  31159  unopf1o  32003  ballotlemrv  34697  subfacp1lem3  35395  subfacp1lem5  35397  wl-sbcom2d  37810  poimirlem26  37891  areacirclem1  37953  areacirc  37958  cdleme50eq  40911  hdmapeq0  42214  hdmap11  42218  ef11d  42703  rmxdiophlem  43366  ordeldif1o  43611  ceilbi  47687  nnsum3primesle9  48148