Theorem 3bitr2rd 311

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr2d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))
3bitr2d.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitr2rd	⊢ (𝜑 → (𝜏 ↔ 𝜓))

Proof of Theorem 3bitr2rd

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitr2d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	1, 2	bitr4d 285	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitr2d 283	1 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  fnsuppres  8201  addsubeq4  11565  muleqadd  11953  mulle0b  12181  adddivflid  13951  om2uzlti  14086  summodnegmod  16449  qnumdenbi  16913  dprdf11  20232  lvecvscan2  21383  mdetunilem9  22928  elfilss  24188  mbfmulc2lem  25961  itg2seq  26056  itg2cnlem2  26076  chpchtsum  27539  bposlem7  27610  lgsdilem  27644  lgsne0  27655  n0lts1e0  28747  colhp  29241  axcontlem7  29541  pjnorm2  32322  cdj3lem1  33029  receqid  33329  rlocisunit  33830  zringfrac  34079  ply1dg1rt  34105  zrhchr  34599  bj-gabima  37833  dochfln0  42514  mapdindp  42708  stgredgiun  49025