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  9484  ltaddsub  11615  leaddsub  11617  eqneg  11865  sqreulem  15287  brcic  17726  nmzsubg  19098  f1omvdconj  19379  dfod2  19497  odf1o2  19506  cyggenod  19817  0ringdif  20464  lvecvscan  21070  znidomb  21520  mdetunilem9  22568  iccpnfcnv  24902  dvcvx  25985  cxple2  26666  wilthlem1  27038  lgslem1  27268  eucliddivs  28355  colinearalglem2  28963  axeuclidlem  29018  axcontlem7  29026  fusgrfisstep  29385  hvmulcan  31130  unopf1o  31974  ballotlemrv  34658  subfacp1lem3  35357  subfacp1lem5  35359  wl-sbcom2d  37737  poimirlem26  37818  areacirclem1  37880  areacirc  37885  cdleme50eq  40838  hdmapeq0  42141  hdmap11  42145  ef11d  42630  rmxdiophlem  43293  ordeldif1o  43538  ceilbi  47615  nnsum3primesle9  48076