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 206

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 207

This theorem is referenced by:  wdomtr  9616  ltaddsub  11738  leaddsub  11740  eqneg  11988  sqreulem  15399  brcic  17843  nmzsubg  19184  f1omvdconj  19465  dfod2  19583  odf1o2  19592  cyggenod  19903  0ringdif  20528  lvecvscan  21114  znidomb  21581  mdetunilem9  22627  iccpnfcnv  24976  dvcvx  26060  cxple2  26740  wilthlem1  27112  lgslem1  27342  colinearalglem2  28923  axeuclidlem  28978  axcontlem7  28986  fusgrfisstep  29347  hvmulcan  31092  unopf1o  31936  ballotlemrv  34523  subfacp1lem3  35188  subfacp1lem5  35190  wl-sbcom2d  37563  poimirlem26  37654  areacirclem1  37716  areacirc  37721  cdleme50eq  40544  hdmapeq0  41847  hdmap11  41851  ef11d  42380  rmxdiophlem  43032  ordeldif1o  43278  nnsum3primesle9  47786