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  9456  ltaddsub  11583  leaddsub  11585  eqneg  11833  sqreulem  15259  brcic  17697  nmzsubg  19070  f1omvdconj  19351  dfod2  19469  odf1o2  19478  cyggenod  19789  0ringdif  20435  lvecvscan  21041  znidomb  21491  mdetunilem9  22528  iccpnfcnv  24862  dvcvx  25945  cxple2  26626  wilthlem1  26998  lgslem1  27228  eucliddivs  28294  colinearalglem2  28878  axeuclidlem  28933  axcontlem7  28941  fusgrfisstep  29300  hvmulcan  31042  unopf1o  31886  ballotlemrv  34523  subfacp1lem3  35194  subfacp1lem5  35196  wl-sbcom2d  37574  poimirlem26  37665  areacirclem1  37727  areacirc  37732  cdleme50eq  40559  hdmapeq0  41862  hdmap11  41866  ef11d  42351  rmxdiophlem  43027  ordeldif1o  43272  ceilbi  47343  nnsum3primesle9  47804