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  9042  ltaddsub  11117  leaddsub  11119  eqneg  11363  sqreulem  14722  brcic  17071  nmzsubg  18320  f1omvdconj  18577  dfod2  18694  odf1o2  18701  cyggenod  19006  lvecvscan  19886  znidomb  20711  mdetunilem9  21232  iccpnfcnv  23551  dvcvx  24620  cxple2  25283  wilthlem1  25648  lgslem1  25876  colinearalglem2  26696  axeuclidlem  26751  axcontlem7  26759  fusgrfisstep  27114  hvmulcan  28852  unopf1o  29696  ballotlemrv  31781  subfacp1lem3  32433  subfacp1lem5  32435  wl-sbcom2d  34801  poimirlem26  34922  areacirclem1  34986  areacirc  34991  cdleme50eq  37681  hdmapeq0  38984  hdmap11  38988  rmxdiophlem  39618  nnsum3primesle9  43966  0ringdif  44148