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  9547  ltaddsub  11706  leaddsub  11708  eqneg  11953  sqreulem  15437  brcic  17880  nmzsubg  19262  f1omvdconj  19547  dfod2  19665  odf1o2  19674  cyggenod  19985  0ringdif  20662  lvecvscan  21272  znidomb  21748  mdetunilem9  22814  iccpnfcnv  25140  dvcvx  26216  cxple2  26899  wilthlem1  27269  lgslem1  27498  eucliddivs  28606  colinearalglem2  29294  axeuclidlem  29349  axcontlem7  29357  fusgrfisstep  29716  hvmulcan  31461  unopf1o  32305  ballotlemrv  34942  subfacp1lem3  35695  subfacp1lem5  35697  wl-sbcom2d  38257  poimirlem26  38338  areacirclem1  38400  areacirc  38405  cdleme50eq  41356  hdmapeq0  42659  hdmap11  42663  ef11d  43141  rmxdiophlem  43783  ordeldif1o  44028  ceilbi  48115  nnsum3primesle9  48600