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  9569  ltaddsub  11687  leaddsub  11689  eqneg  11933  sqreulem  15305  brcic  17744  nmzsubg  19044  f1omvdconj  19313  dfod2  19431  odf1o2  19440  cyggenod  19751  lvecvscan  20723  znidomb  21116  mdetunilem9  22121  iccpnfcnv  24459  dvcvx  25536  cxple2  26204  wilthlem1  26569  lgslem1  26797  colinearalglem2  28162  axeuclidlem  28217  axcontlem7  28225  fusgrfisstep  28583  hvmulcan  30320  unopf1o  31164  ballotlemrv  33513  subfacp1lem3  34168  subfacp1lem5  34170  wl-sbcom2d  36421  poimirlem26  36509  areacirclem1  36571  areacirc  36576  cdleme50eq  39407  hdmapeq0  40710  hdmap11  40714  rmxdiophlem  41744  ordeldif1o  42000  nnsum3primesle9  46452  0ringdif  46634