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  8183  addsubeq4  11468  muleqadd  11854  mulle0b  12082  adddivflid  13847  om2uzlti  13982  summodnegmod  16340  qnumdenbi  16799  dprdf11  20091  lvecvscan2  21210  mdetunilem9  22742  elfilss  23998  mbfmulc2lem  25771  itg2seq  25866  itg2cnlem2  25886  chpchtsum  27345  bposlem7  27416  lgsdilem  27450  lgsne0  27461  n0lts1e0  28523  colhp  29007  axcontlem7  29257  pjnorm2  32016  cdj3lem1  32723  receqid  33026  rlocisunit  33533  zringfrac  33785  ply1dg1rt  33811  zrhchr  34305  bj-gabima  37460  dochfln0  42136  mapdindp  42330  stgredgiun  48605