Theorem syl5ibcom 211

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

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

Assertion

Ref	Expression
syl5ibcom	⊢ (φ → (χ → θ))

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 ⊢ (φ → ψ)
2		syl5ib.2	. . 3 ⊢ (χ → (ψ ↔ θ))
3	1, 2	syl5ib 210	. 2 ⊢ (χ → (φ → θ))
4	3	com12 27	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:  biimpcd  215  mob2  3016  rmob  3134  ltfintri  4466  ncfineleq  4477  tfinltfin  4501  tfinnn  4534  sfinltfin  4535  vfinncvntnn  4548  vfinspsslem1  4550  phi11lem1  4595  phialllem1  4616  xp11  5056  tz6.12c  5347  weds  5938  erth  5968  ectocld  5991  ecoptocl  5996  mapsn  6026  fndmeng  6046  enmap1lem3  6071  enprmaplem6  6081  ltlenlec  6207  nchoicelem9  6297