Theorem 3bitr3rd 302

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  wdomtr  8720  ltaddsub  10792  leaddsub  10794  eqneg  11035  sqreulem  14437  brcic  16769  nmzsubg  17945  f1omvdconj  18175  dfod2  18291  odf1o2  18298  cyggenod  18598  lvecvscan  19429  znidomb  20228  mdetunilem9  20749  iccpnfcnv  23068  dvcvx  24121  cxple2  24781  wilthlem1  25143  lgslem1  25371  colinearalglem2  26136  axeuclidlem  26191  axcontlem7  26199  fusgrfisstep  26555  hvmulcan  28446  unopf1o  29292  ballotlemrv  31090  subfacp1lem3  31673  subfacp1lem5  31675  wl-sbcom2d  33826  poimirlem26  33916  areacirclem1  33980  areacirc  33985  cdleme50eq  36554  hdmapeq0  37857  hdmap11  37861  rmxdiophlem  38355  nnsum3primesle9  42452  0ringdif  42657