Theorem 3bitr3rd 309

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  wdomtr  9264  ltaddsub  11379  leaddsub  11381  eqneg  11625  sqreulem  14999  brcic  17427  nmzsubg  18708  f1omvdconj  18969  dfod2  19086  odf1o2  19093  cyggenod  19399  lvecvscan  20288  znidomb  20681  mdetunilem9  21677  iccpnfcnv  24013  dvcvx  25089  cxple2  25757  wilthlem1  26122  lgslem1  26350  colinearalglem2  27178  axeuclidlem  27233  axcontlem7  27241  fusgrfisstep  27599  hvmulcan  29335  unopf1o  30179  ballotlemrv  32386  subfacp1lem3  33044  subfacp1lem5  33046  wl-sbcom2d  35643  poimirlem26  35730  areacirclem1  35792  areacirc  35797  cdleme50eq  38482  hdmapeq0  39785  hdmap11  39789  rmxdiophlem  40753  nnsum3primesle9  45134  0ringdif  45316