Theorem 3bitr2rd 311

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 285	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitr2d 283	1 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  fnsuppres  8189  addsubeq4  11483  muleqadd  11869  mulle0b  12097  adddivflid  13865  om2uzlti  14000  summodnegmod  16362  qnumdenbi  16821  dprdf11  20119  lvecvscan2  21266  mdetunilem9  22807  elfilss  24064  mbfmulc2lem  25837  itg2seq  25932  itg2cnlem2  25952  chpchtsum  27414  bposlem7  27485  lgsdilem  27519  lgsne0  27530  n0lts1e0  28592  colhp  29083  axcontlem7  29351  pjnorm2  32126  cdj3lem1  32833  receqid  33135  rlocisunit  33636  zringfrac  33884  ply1dg1rt  33910  zrhchr  34404  bj-gabima  37609  dochfln0  42284  mapdindp  42478  stgredgiun  48756