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  9112  ltaddsub  11192  leaddsub  11194  eqneg  11438  sqreulem  14809  brcic  17173  nmzsubg  18435  f1omvdconj  18692  dfod2  18809  odf1o2  18816  cyggenod  19122  lvecvscan  20002  znidomb  20380  mdetunilem9  21371  iccpnfcnv  23696  dvcvx  24772  cxple2  25440  wilthlem1  25805  lgslem1  26033  colinearalglem2  26853  axeuclidlem  26908  axcontlem7  26916  fusgrfisstep  27271  hvmulcan  29007  unopf1o  29851  ballotlemrv  32056  subfacp1lem3  32715  subfacp1lem5  32717  wl-sbcom2d  35339  poimirlem26  35426  areacirclem1  35488  areacirc  35493  cdleme50eq  38178  hdmapeq0  39481  hdmap11  39485  rmxdiophlem  40409  nnsum3primesle9  44780  0ringdif  44962