Theorem 3bitr3rd 299

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  wdomtr  8635  ltaddsub  10703  leaddsub  10705  eqneg  10946  sqreulem  14306  brcic  16664  nmzsubg  17842  f1omvdconj  18072  dfod2  18187  odf1o2  18194  cyggenod  18492  lvecvscan  19323  znidomb  20124  mdetunilem9  20643  iccpnfcnv  22962  dvcvx  24002  cxple2  24663  wilthlem1  25014  lgslem1  25242  colinearalglem2  26007  axeuclidlem  26062  axcontlem7  26070  fusgrfisstep  26443  hvmulcan  28266  unopf1o  29112  ballotlemrv  30918  subfacp1lem3  31499  subfacp1lem5  31501  wl-sbcom2d  33674  poimirlem26  33764  areacirclem1  33828  areacirc  33833  cdleme50eq  36346  hdmapeq0  37650  hdmap11  37654  rmxdiophlem  38104  nnsum3primesle9  42206  0ringdif  42394