Theorem 3bitr3rd 313

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  wdomtr  9525  ltaddsub  11676  leaddsub  11678  eqneg  11926  sqreulem  15401  brcic  17845  nmzsubg  19222  f1omvdconj  19507  dfod2  19625  odf1o2  19634  cyggenod  19945  0ringdif  20602  lvecvscan  21204  znidomb  21671  mdetunilem9  22738  iccpnfcnv  25064  dvcvx  26140  cxple2  26820  wilthlem1  27190  lgslem1  27419  eucliddivs  28527  colinearalglem2  29166  axeuclidlem  29221  axcontlem7  29229  fusgrfisstep  29588  hvmulcan  31333  unopf1o  32177  ballotlemrv  34827  subfacp1lem3  35545  subfacp1lem5  35547  wl-sbcom2d  38076  poimirlem26  38157  areacirclem1  38219  areacirc  38224  cdleme50eq  41177  hdmapeq0  42480  hdmap11  42484  ef11d  42960  rmxdiophlem  43604  ordeldif1o  43849  ceilbi  47929  nnsum3primesle9  48414