Theorem 3bitr2rd 297

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  fnsuppres  7322  addsubeq4  10296  muleqadd  10671  mulle0b  10894  adddivflid  12619  om2uzlti  12749  summodnegmod  15012  qnumdenbi  15452  dprdf11  18422  lvecvscan2  19112  mdetunilem9  20426  elfilss  21680  itg2seq  23509  itg2cnlem2  23529  chpchtsum  24944  bposlem7  25015  lgsdilem  25049  lgsne0  25060  colhp  25662  axcontlem7  25850  pjnorm2  28586  cdj3lem1  29293  zrhchr  30020  dochfln0  36766  mapdindp  36960