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 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  9570  ltaddsub  11688  leaddsub  11690  eqneg  11934  sqreulem  15306  brcic  17745  nmzsubg  19045  f1omvdconj  19314  dfod2  19432  odf1o2  19441  cyggenod  19752  lvecvscan  20724  znidomb  21117  mdetunilem9  22122  iccpnfcnv  24460  dvcvx  25537  cxple2  26205  wilthlem1  26572  lgslem1  26800  colinearalglem2  28165  axeuclidlem  28220  axcontlem7  28228  fusgrfisstep  28586  hvmulcan  30325  unopf1o  31169  ballotlemrv  33518  subfacp1lem3  34173  subfacp1lem5  34175  wl-sbcom2d  36426  poimirlem26  36514  areacirclem1  36576  areacirc  36581  cdleme50eq  39412  hdmapeq0  40715  hdmap11  40719  rmxdiophlem  41754  ordeldif1o  42010  nnsum3primesle9  46462  0ringdif  46644