Theorem 3bitr3rd 312

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  wdomtr  9520  ltaddsub  11658  leaddsub  11660  eqneg  11908  sqreulem  15370  brcic  17814  nmzsubg  19189  f1omvdconj  19469  dfod2  19587  odf1o2  19596  cyggenod  19907  0ringdif  20556  lvecvscan  21161  znidomb  21593  mdetunilem9  22660  iccpnfcnv  24986  dvcvx  26062  cxple2  26739  wilthlem1  27109  lgslem1  27338  eucliddivs  28446  colinearalglem2  29054  axeuclidlem  29109  axcontlem7  29117  fusgrfisstep  29476  hvmulcan  31221  unopf1o  32065  ballotlemrv  34778  subfacp1lem3  35496  subfacp1lem5  35498  wl-sbcom2d  38028  poimirlem26  38109  areacirclem1  38171  areacirc  38176  cdleme50eq  41129  hdmapeq0  42432  hdmap11  42436  ef11d  42912  rmxdiophlem  43556  ordeldif1o  43801  ceilbi  47895  nnsum3primesle9  48380