Theorem mpisyl 1457

Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.)

Hypotheses

Ref	Expression
mpisyl.1	|- ( ph -> ps )
mpisyl.2	|- ch
mpisyl.3	|- ( ps -> ( ch -> th ) )

Assertion

Ref	Expression
mpisyl	|- ( ph -> th )

Proof of Theorem mpisyl

Step	Hyp	Ref	Expression
1		mpisyl.1	. 2 |- ( ph -> ps )
2		mpisyl.2	. . 3 |- ch
3		mpisyl.3	. . 3 |- ( ps -> ( ch -> th ) )
4	2, 3	mpi 15	. 2 |- ( ps -> th )
5	1, 4	syl 14	1 |- ( ph -> th )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  ceqsex  2801  reusv1  4493  iotaexab  5237  fliftcnv  5842  fliftfun  5843  tfrlemibfn  6386  tfr1onlembfn  6402  tfrcllembfn  6415  cnvct  6868  ordiso  7102  exmidomni  7208  djudoml  7286  djudomr  7287  uzsinds  10536  fimaxq  10919  ltoddhalfle  12058  phicl2  12382  strsetsid  12711  txdis1cn  14514  xmeter  14672  2lgslem1  15332  subctctexmid  15645