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  8195  addsubeq4  11502  muleqadd  11886  mulle0b  12118  adddivflid  13840  om2uzlti  13973  summodnegmod  16311  qnumdenbi  16768  dprdf11  20011  lvecvscan2  21078  mdetunilem9  22563  elfilss  23819  mbfmulc2lem  25605  itg2seq  25700  itg2cnlem2  25720  chpchtsum  27187  bposlem7  27258  lgsdilem  27292  lgsne0  27303  colhp  28754  axcontlem7  28954  pjnorm2  31713  cdj3lem1  32420  receqid  32727  zringfrac  33574  ply1dg1rt  33597  zrhchr  34010  bj-gabima  36963  dochfln0  41501  mapdindp  41695  stgredgiun  47937