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  9490  ltaddsub  11624  leaddsub  11626  eqneg  11875  sqreulem  15322  brcic  17765  nmzsubg  19140  f1omvdconj  19421  dfod2  19539  odf1o2  19548  cyggenod  19859  0ringdif  20504  lvecvscan  21109  znidomb  21541  mdetunilem9  22585  iccpnfcnv  24911  dvcvx  25987  cxple2  26661  wilthlem1  27031  lgslem1  27260  eucliddivs  28368  colinearalglem2  28976  axeuclidlem  29031  axcontlem7  29039  fusgrfisstep  29398  hvmulcan  31143  unopf1o  31987  ballotlemrv  34664  subfacp1lem3  35364  subfacp1lem5  35366  wl-sbcom2d  37886  poimirlem26  37967  areacirclem1  38029  areacirc  38034  cdleme50eq  40987  hdmapeq0  42290  hdmap11  42294  ef11d  42771  rmxdiophlem  43443  ordeldif1o  43688  ceilbi  47785  nnsum3primesle9  48270