Theorem 3bitr3rd 298

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  wdomtr  8363  ltaddsub  10381  leaddsub  10383  eqneg  10624  sqreulem  13947  brcic  16281  nmzsubg  17458  f1omvdconj  17689  dfod2  17804  odf1o2  17811  cyggenod  18109  lvecvscan  18932  znidomb  19729  mdetunilem9  20245  iccpnfcnv  22551  dvcvx  23587  cxple2  24243  wilthlem1  24594  lgslem1  24822  colinearalglem2  25587  axeuclidlem  25642  axcontlem7  25650  hvmulcan  27313  unopf1o  28159  ballotlemrv  29908  subfacp1lem3  30418  subfacp1lem5  30420  wl-sbcom2d  32523  poimirlem26  32605  areacirclem1  32670  areacirc  32675  cdleme50eq  34847  hdmapeq0  36154  hdmap11  36158  rmxdiophlem  36600  nnsum3primesle9  40210  fusgrfisstep  40548  0ringdif  41660