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  8131  addsubeq4  11397  muleqadd  11783  mulle0b  12015  adddivflid  13741  om2uzlti  13876  summodnegmod  16216  qnumdenbi  16674  dprdf11  19923  lvecvscan2  21038  mdetunilem9  22524  elfilss  23780  mbfmulc2lem  25565  itg2seq  25660  itg2cnlem2  25680  chpchtsum  27147  bposlem7  27218  lgsdilem  27252  lgsne0  27263  colhp  28734  axcontlem7  28934  pjnorm2  31690  cdj3lem1  32397  receqid  32707  zringfrac  33510  ply1dg1rt  33534  zrhchr  33960  bj-gabima  36933  dochfln0  41476  mapdindp  41670  stgredgiun  47962