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  7840  addsubeq4  10890  muleqadd  11273  mulle0b  11500  adddivflid  13183  om2uzlti  13313  summodnegmod  15632  qnumdenbi  16074  dprdf11  19138  lvecvscan2  19877  mdetunilem9  21225  elfilss  22481  mbfmulc2lem  24251  itg2seq  24346  itg2cnlem2  24366  chpchtsum  25803  bposlem7  25874  lgsdilem  25908  lgsne0  25919  colhp  26564  axcontlem7  26764  pjnorm2  29510  cdj3lem1  30217  zrhchr  31327  dochfln0  38773  mapdindp  38967