Theorem 3bitr3rd 313

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  wdomtr  9538  ltaddsub  11689  leaddsub  11691  eqneg  11936  sqreulem  15413  brcic  17856  nmzsubg  19232  f1omvdconj  19517  dfod2  19635  odf1o2  19644  cyggenod  19955  0ringdif  20612  lvecvscan  21216  znidomb  21692  mdetunilem9  22758  iccpnfcnv  25084  dvcvx  26160  cxple2  26840  wilthlem1  27210  lgslem1  27439  eucliddivs  28547  colinearalglem2  29235  axeuclidlem  29290  axcontlem7  29298  fusgrfisstep  29657  hvmulcan  31402  unopf1o  32246  ballotlemrv  34888  subfacp1lem3  35652  subfacp1lem5  35654  wl-sbcom2d  38194  poimirlem26  38275  areacirclem1  38337  areacirc  38342  cdleme50eq  41293  hdmapeq0  42596  hdmap11  42600  ef11d  43078  rmxdiophlem  43722  ordeldif1o  43967  ceilbi  48051  nnsum3primesle9  48536