Theorem syl5ibr 212

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)

Hypotheses

Ref	Expression
syl5ibr.1	⊢ (φ → θ)
syl5ibr.2	⊢ (χ → (ψ ↔ θ))

Assertion

Ref	Expression
syl5ibr	⊢ (χ → (φ → ψ))

Proof of Theorem syl5ibr

Step	Hyp	Ref	Expression
1		syl5ibr.1	. 2 ⊢ (φ → θ)
2		syl5ibr.2	. . 3 ⊢ (χ → (ψ ↔ θ))
3	2	bicomd 192	. 2 ⊢ (χ → (θ ↔ ψ))
4	1, 3	syl5ib 210	1 ⊢ (χ → (φ → ψ))

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  syl5ibrcom  213  biimprd  214  dvelimv  1939  pm2.61ne  2591  unineq  3505  sspw1  4335  vfinncvntnn  4548  ffvresb  5431  peano4nc  6150  ce0addcnnul  6179  ce0nn  6180  ceclb  6183  dflec2  6210  ce0lenc1  6239  addcdi  6250  nchoicelem17  6305  frecxp  6314