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  7491  addsubeq4  10488  muleqadd  10863  mulle0b  11086  adddivflid  12813  om2uzlti  12943  summodnegmod  15214  qnumdenbi  15654  dprdf11  18622  lvecvscan2  19314  mdetunilem9  20628  elfilss  21881  itg2seq  23708  itg2cnlem2  23728  chpchtsum  25143  bposlem7  25214  lgsdilem  25248  lgsne0  25259  colhp  25861  axcontlem7  26049  pjnorm2  28895  cdj3lem1  29602  zrhchr  30329  dochfln0  37268  mapdindp  37462