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  9644  ltaddsub  11764  leaddsub  11766  eqneg  12014  sqreulem  15408  brcic  17859  nmzsubg  19205  f1omvdconj  19488  dfod2  19606  odf1o2  19615  cyggenod  19926  0ringdif  20553  lvecvscan  21136  znidomb  21603  mdetunilem9  22647  iccpnfcnv  24994  dvcvx  26079  cxple2  26757  wilthlem1  27129  lgslem1  27359  colinearalglem2  28940  axeuclidlem  28995  axcontlem7  29003  fusgrfisstep  29364  hvmulcan  31104  unopf1o  31948  ballotlemrv  34484  subfacp1lem3  35150  subfacp1lem5  35152  wl-sbcom2d  37515  poimirlem26  37606  areacirclem1  37668  areacirc  37673  cdleme50eq  40498  hdmapeq0  41801  hdmap11  41805  ef11d  42327  rmxdiophlem  42972  ordeldif1o  43222  nnsum3primesle9  47668