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-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  syl5ibrcom  213  biimprd  214  dvelimv  1939  pm2.61ne  2592  unineq  3506  sspw1  4336  vfinncvntnn  4549  ffvresb  5432  peano4nc  6151  ce0addcnnul  6180  ce0nn  6181  ceclb  6184  dflec2  6211  ce0lenc1  6240  addcdi  6251  nchoicelem17  6306  frecxp  6315