Theorem 3bitr3rd 312

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 283	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
5	1, 4	bitr3d 283	1 ⊢ (𝜑 → (𝜏 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  wdomtr  9033  ltaddsub  11108  leaddsub  11110  eqneg  11354  sqreulem  14713  brcic  17062  nmzsubg  18311  f1omvdconj  18568  dfod2  18685  odf1o2  18692  cyggenod  18997  lvecvscan  19877  znidomb  20702  mdetunilem9  21223  iccpnfcnv  23542  dvcvx  24611  cxple2  25274  wilthlem1  25639  lgslem1  25867  colinearalglem2  26687  axeuclidlem  26742  axcontlem7  26750  fusgrfisstep  27105  hvmulcan  28843  unopf1o  29687  ballotlemrv  31772  subfacp1lem3  32424  subfacp1lem5  32426  wl-sbcom2d  34791  poimirlem26  34912  areacirclem1  34976  areacirc  34981  cdleme50eq  37671  hdmapeq0  38974  hdmap11  38978  rmxdiophlem  39605  nnsum3primesle9  43952  0ringdif  44134