Theorem mpisyl 1489

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  2839  reusv1  4553  iotaexab  5303  fliftcnv  5931  fliftfun  5932  tfrlemibfn  6489  tfr1onlembfn  6505  tfrcllembfn  6518  cnvct  6979  ordiso  7226  exmidomni  7332  djudoml  7424  djudomr  7425  uzsinds  10696  fimaxq  11081  ltoddhalfle  12444  phicl2  12776  strsetsid  13105  txdis1cn  14992  xmeter  15150  2lgslem1  15810  usgredg2v  16063  1loopgrvd2fi  16111  subctctexmid  16537