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  9494  ltaddsub  11625  leaddsub  11627  eqneg  11875  sqreulem  15297  brcic  17736  nmzsubg  19111  f1omvdconj  19392  dfod2  19510  odf1o2  19519  cyggenod  19830  0ringdif  20477  lvecvscan  21083  znidomb  21533  mdetunilem9  22581  iccpnfcnv  24915  dvcvx  25998  cxple2  26679  wilthlem1  27051  lgslem1  27281  eucliddivs  28389  colinearalglem2  28998  axeuclidlem  29053  axcontlem7  29061  fusgrfisstep  29420  hvmulcan  31166  unopf1o  32010  ballotlemrv  34704  subfacp1lem3  35404  subfacp1lem5  35406  wl-sbcom2d  37845  poimirlem26  37926  areacirclem1  37988  areacirc  37993  cdleme50eq  40946  hdmapeq0  42249  hdmap11  42253  ef11d  42738  rmxdiophlem  43401  ordeldif1o  43646  ceilbi  47722  nnsum3primesle9  48183