Theorem 3bitr2rd 307

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 281	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitr2d 279	1 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  fnsuppres  8179  addsubeq4  11480  muleqadd  11863  mulle0b  12090  adddivflid  13788  om2uzlti  13920  summodnegmod  16235  qnumdenbi  16685  dprdf11  19935  lvecvscan2  20871  mdetunilem9  22343  elfilss  23601  mbfmulc2lem  25397  itg2seq  25493  itg2cnlem2  25513  chpchtsum  26955  bposlem7  27026  lgsdilem  27060  lgsne0  27071  colhp  28285  axcontlem7  28492  pjnorm2  31244  cdj3lem1  31951  zrhchr  33251  bj-gabima  36124  dochfln0  40652  mapdindp  40846