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  9528  ltaddsub  11652  leaddsub  11654  eqneg  11902  sqreulem  15326  brcic  17760  nmzsubg  19097  f1omvdconj  19376  dfod2  19494  odf1o2  19503  cyggenod  19814  0ringdif  20436  lvecvscan  21021  znidomb  21471  mdetunilem9  22507  iccpnfcnv  24842  dvcvx  25925  cxple2  26606  wilthlem1  26978  lgslem1  27208  eucliddivs  28265  colinearalglem2  28834  axeuclidlem  28889  axcontlem7  28897  fusgrfisstep  29256  hvmulcan  31001  unopf1o  31845  ballotlemrv  34511  subfacp1lem3  35169  subfacp1lem5  35171  wl-sbcom2d  37549  poimirlem26  37640  areacirclem1  37702  areacirc  37707  cdleme50eq  40535  hdmapeq0  41838  hdmap11  41842  ef11d  42327  rmxdiophlem  43004  ordeldif1o  43249  ceilbi  47334  nnsum3primesle9  47795