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 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  fnsuppres  8188  addsubeq4  11473  muleqadd  11859  mulle0b  12087  adddivflid  13853  om2uzlti  13988  summodnegmod  16345  qnumdenbi  16804  dprdf11  20096  lvecvscan2  21217  mdetunilem9  22758  elfilss  24014  mbfmulc2lem  25787  itg2seq  25882  itg2cnlem2  25902  chpchtsum  27364  bposlem7  27435  lgsdilem  27469  lgsne0  27480  n0lts1e0  28542  colhp  29033  axcontlem7  29301  pjnorm2  32060  cdj3lem1  32767  receqid  33070  rlocisunit  33577  zringfrac  33825  ply1dg1rt  33851  zrhchr  34345  bj-gabima  37557  dochfln0  42232  mapdindp  42426  stgredgiun  48706