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 205

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 206

This theorem is referenced by:  wdomtr  9590  ltaddsub  11710  leaddsub  11712  eqneg  11956  sqreulem  15330  brcic  17772  nmzsubg  19111  f1omvdconj  19392  dfod2  19510  odf1o2  19519  cyggenod  19830  0ringdif  20453  lvecvscan  20988  znidomb  21482  mdetunilem9  22509  iccpnfcnv  24856  dvcvx  25940  cxple2  26618  wilthlem1  26987  lgslem1  27217  colinearalglem2  28705  axeuclidlem  28760  axcontlem7  28768  fusgrfisstep  29129  hvmulcan  30869  unopf1o  31713  ballotlemrv  34075  subfacp1lem3  34728  subfacp1lem5  34730  wl-sbcom2d  36963  poimirlem26  37054  areacirclem1  37116  areacirc  37121  cdleme50eq  39951  hdmapeq0  41254  hdmap11  41258  ef11d  41832  rmxdiophlem  42358  ordeldif1o  42612  nnsum3primesle9  47057