Theorem mpisyl 1422

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  2719  reusv1  4374  fliftcnv  5689  fliftfun  5690  tfrlemibfn  6218  tfr1onlembfn  6234  tfrcllembfn  6247  cnvct  6696  ordiso  6914  exmidomni  7007  djudoml  7068  djudomr  7069  uzsinds  10208  fimaxq  10566  ltoddhalfle  11579  phicl2  11879  strsetsid  11981  txdis1cn  12436  xmeter  12594  subctctexmid  13185