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 206

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 207

This theorem is referenced by:  wdomtr  9594  ltaddsub  11716  leaddsub  11718  eqneg  11966  sqreulem  15383  brcic  17816  nmzsubg  19153  f1omvdconj  19432  dfod2  19550  odf1o2  19559  cyggenod  19870  0ringdif  20492  lvecvscan  21077  znidomb  21527  mdetunilem9  22563  iccpnfcnv  24898  dvcvx  25982  cxple2  26663  wilthlem1  27035  lgslem1  27265  eucliddivs  28322  colinearalglem2  28891  axeuclidlem  28946  axcontlem7  28954  fusgrfisstep  29313  hvmulcan  31058  unopf1o  31902  ballotlemrv  34557  subfacp1lem3  35209  subfacp1lem5  35211  wl-sbcom2d  37584  poimirlem26  37675  areacirclem1  37737  areacirc  37742  cdleme50eq  40565  hdmapeq0  41868  hdmap11  41872  ef11d  42355  rmxdiophlem  43006  ordeldif1o  43251  ceilbi  47329  nnsum3primesle9  47775