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  8246  addsubeq4  11611  muleqadd  12000  mulle0b  12228  adddivflid  13998  om2uzlti  14133  summodnegmod  16500  qnumdenbi  16964  dprdf11  20290  lvecvscan2  21441  mdetunilem9  22990  elfilss  24250  mbfmulc2lem  26023  itg2seq  26118  itg2cnlem2  26138  chpchtsum  27603  bposlem7  27674  lgsdilem  27708  lgsne0  27719  n0lts1e0  28811  colhp  29305  axcontlem7  29605  pjnorm2  32386  cdj3lem1  33093  receqid  33432  rlocisunit  33936  zringfrac  34189  ply1dg1rt  34215  zrhchr  34717  bj-gabima  38068  dochfln0  42800  mapdindp  42994  stgredgiun  49329