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  9486  ltaddsub  11612  leaddsub  11614  eqneg  11862  sqreulem  15285  brcic  17723  nmzsubg  19062  f1omvdconj  19343  dfod2  19461  odf1o2  19470  cyggenod  19781  0ringdif  20430  lvecvscan  21036  znidomb  21486  mdetunilem9  22523  iccpnfcnv  24858  dvcvx  25941  cxple2  26622  wilthlem1  26994  lgslem1  27224  eucliddivs  28288  colinearalglem2  28870  axeuclidlem  28925  axcontlem7  28933  fusgrfisstep  29292  hvmulcan  31034  unopf1o  31878  ballotlemrv  34487  subfacp1lem3  35154  subfacp1lem5  35156  wl-sbcom2d  37534  poimirlem26  37625  areacirclem1  37687  areacirc  37692  cdleme50eq  40520  hdmapeq0  41823  hdmap11  41827  ef11d  42312  rmxdiophlem  42988  ordeldif1o  43233  ceilbi  47318  nnsum3primesle9  47779