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  8130  addsubeq4  11386  muleqadd  11772  mulle0b  12004  adddivflid  13729  om2uzlti  13864  summodnegmod  16204  qnumdenbi  16662  dprdf11  19945  lvecvscan2  21058  mdetunilem9  22555  elfilss  23811  mbfmulc2lem  25595  itg2seq  25690  itg2cnlem2  25710  chpchtsum  27177  bposlem7  27248  lgsdilem  27282  lgsne0  27293  colhp  28768  axcontlem7  28969  pjnorm2  31728  cdj3lem1  32435  receqid  32752  zringfrac  33563  ply1dg1rt  33589  zrhchr  34059  bj-gabima  37057  dochfln0  41649  mapdindp  41843  stgredgiun  48120