Theorem syl5ibcom 211

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

Hypotheses

Ref	Expression
syl5ib.1	|- (ph -> ps)
syl5ib.2	|- (ch -> (ps <-> th))

Assertion

Ref	Expression
syl5ibcom	|- (ph -> (ch -> th))

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 |- (ph -> ps)
2		syl5ib.2	. . 3 |- (ch -> (ps <-> th))
3	1, 2	syl5ib 210	. 2 |- (ch -> (ph -> th))
4	3	com12 27	1 |- (ph -> (ch -> th))

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  3017  rmob  3135  ltfintri  4467  ncfineleq  4478  tfinltfin  4502  tfinnn  4535  sfinltfin  4536  vfinncvntnn  4549  vfinspsslem1  4551  phi11lem1  4596  phialllem1  4617  xp11  5057  tz6.12c  5348  weds  5939  erth  5969  ectocld  5992  ecoptocl  5997  mapsn  6027  fndmeng  6047  enmap1lem3  6072  enprmaplem6  6082  ltlenlec  6208  nchoicelem9  6298