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  9535  ltaddsub  11659  leaddsub  11661  eqneg  11909  sqreulem  15333  brcic  17767  nmzsubg  19104  f1omvdconj  19383  dfod2  19501  odf1o2  19510  cyggenod  19821  0ringdif  20443  lvecvscan  21028  znidomb  21478  mdetunilem9  22514  iccpnfcnv  24849  dvcvx  25932  cxple2  26613  wilthlem1  26985  lgslem1  27215  eucliddivs  28272  colinearalglem2  28841  axeuclidlem  28896  axcontlem7  28904  fusgrfisstep  29263  hvmulcan  31008  unopf1o  31852  ballotlemrv  34518  subfacp1lem3  35176  subfacp1lem5  35178  wl-sbcom2d  37556  poimirlem26  37647  areacirclem1  37709  areacirc  37714  cdleme50eq  40542  hdmapeq0  41845  hdmap11  41849  ef11d  42334  rmxdiophlem  43011  ordeldif1o  43256  ceilbi  47338  nnsum3primesle9  47799