Theorem 3bitr3rd 311

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  wdomtr  9487  ltaddsub  11622  leaddsub  11624  eqneg  11873  sqreulem  15320  brcic  17763  nmzsubg  19138  f1omvdconj  19419  dfod2  19537  odf1o2  19546  cyggenod  19857  0ringdif  20506  lvecvscan  21111  znidomb  21543  mdetunilem9  22610  iccpnfcnv  24936  dvcvx  26012  cxple2  26686  wilthlem1  27056  lgslem1  27285  eucliddivs  28393  colinearalglem2  29001  axeuclidlem  29056  axcontlem7  29064  fusgrfisstep  29423  hvmulcan  31168  unopf1o  32012  ballotlemrv  34711  subfacp1lem3  35417  subfacp1lem5  35419  wl-sbcom2d  37939  poimirlem26  38020  areacirclem1  38082  areacirc  38087  cdleme50eq  41040  hdmapeq0  42343  hdmap11  42347  ef11d  42823  rmxdiophlem  43467  ordeldif1o  43712  ceilbi  47807  nnsum3primesle9  48292