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  8132  addsubeq4  11396  muleqadd  11782  mulle0b  12014  adddivflid  13739  om2uzlti  13874  summodnegmod  16214  qnumdenbi  16672  dprdf11  19958  lvecvscan2  21069  mdetunilem9  22563  elfilss  23819  mbfmulc2lem  25592  itg2seq  25687  itg2cnlem2  25707  chpchtsum  27170  bposlem7  27241  lgsdilem  27275  lgsne0  27286  n0lts1e0  28348  colhp  28826  axcontlem7  29027  pjnorm2  31787  cdj3lem1  32494  receqid  32807  zringfrac  33619  ply1dg1rt  33645  zrhchr  34124  bj-gabima  37245  dochfln0  41914  mapdindp  42108  stgredgiun  48392