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  11496  muleqadd  11882  mulle0b  12110  adddivflid  13879  om2uzlti  14014  summodnegmod  16376  qnumdenbi  16835  dprdf11  20152  lvecvscan2  21299  mdetunilem9  22842  elfilss  24102  mbfmulc2lem  25875  itg2seq  25970  itg2cnlem2  25990  chpchtsum  27455  bposlem7  27526  lgsdilem  27560  lgsne0  27571  n0lts1e0  28633  colhp  29127  axcontlem7  29427  pjnorm2  32208  cdj3lem1  32915  receqid  33215  rlocisunit  33716  zringfrac  33964  ply1dg1rt  33990  zrhchr  34484  bj-gabima  37684  dochfln0  42350  mapdindp  42544  stgredgiun  48874