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  9572  ltaddsub  11690  leaddsub  11692  eqneg  11936  sqreulem  15308  brcic  17747  nmzsubg  19047  f1omvdconj  19316  dfod2  19434  odf1o2  19443  cyggenod  19754  lvecvscan  20730  znidomb  21123  mdetunilem9  22129  iccpnfcnv  24467  dvcvx  25544  cxple2  26212  wilthlem1  26579  lgslem1  26807  colinearalglem2  28203  axeuclidlem  28258  axcontlem7  28266  fusgrfisstep  28624  hvmulcan  30363  unopf1o  31207  ballotlemrv  33587  subfacp1lem3  34242  subfacp1lem5  34244  wl-sbcom2d  36512  poimirlem26  36600  areacirclem1  36662  areacirc  36667  cdleme50eq  39498  hdmapeq0  40801  hdmap11  40805  rmxdiophlem  41836  ordeldif1o  42092  nnsum3primesle9  46541  0ringdif  46723