Theorem 3bitr2rd 308

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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitr2d 280	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  8171  addsubeq4  11473  muleqadd  11856  mulle0b  12083  adddivflid  13781  om2uzlti  13913  summodnegmod  16229  qnumdenbi  16681  dprdf11  19937  lvecvscan2  20955  mdetunilem9  22446  elfilss  23704  mbfmulc2lem  25500  itg2seq  25596  itg2cnlem2  25616  chpchtsum  27071  bposlem7  27142  lgsdilem  27176  lgsne0  27187  colhp  28493  axcontlem7  28700  pjnorm2  31452  cdj3lem1  32159  zrhchr  33448  bj-gabima  36311  dochfln0  40842  mapdindp  41036