Theorem 3bitr2rd 308

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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitr2d 280	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:  fnsuppres  8170  addsubeq4  11436  muleqadd  11822  mulle0b  12054  adddivflid  13780  om2uzlti  13915  summodnegmod  16256  qnumdenbi  16714  dprdf11  19955  lvecvscan2  21022  mdetunilem9  22507  elfilss  23763  mbfmulc2lem  25548  itg2seq  25643  itg2cnlem2  25663  chpchtsum  27130  bposlem7  27201  lgsdilem  27235  lgsne0  27246  colhp  28697  axcontlem7  28897  pjnorm2  31656  cdj3lem1  32363  receqid  32668  zringfrac  33525  ply1dg1rt  33548  zrhchr  33964  bj-gabima  36928  dochfln0  41471  mapdindp  41665  stgredgiun  47954