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 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  wdomtr  9596  ltaddsub  11817  leaddsub  11819  eqneg  12064  sqreulem  15556  brcic  18002  nmzsubg  19404  f1omvdconj  19690  dfod2  19808  odf1o2  19817  cyggenod  20128  0ringdif  20808  lvecvscan  21419  znidomb  21897  mdetunilem9  22965  iccpnfcnv  25295  dvcvx  26370  cxple2  27055  wilthlem1  27425  lgslem1  27654  eucliddivs  28792  colinearalglem2  29515  axeuclidlem  29570  axcontlem7  29578  fusgrfisstep  29940  hvmulcan  31704  unopf1o  32548  ballotlemrv  35222  subfacp1lem3  36114  subfacp1lem5  36116  wl-sbcom2d  38685  poimirlem26  38756  areacirclem1  38818  areacirc  38823  cdleme50eq  41790  hdmapeq0  43093  hdmap11  43097  ef11d  43583  rmxdiophlem  44215  ordeldif1o  44454  ceilbi  48612  nnsum3primesle9  49097