Theorem mpisyl 1434

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  2764  reusv1  4436  fliftcnv  5763  fliftfun  5764  tfrlemibfn  6296  tfr1onlembfn  6312  tfrcllembfn  6325  cnvct  6775  ordiso  7001  exmidomni  7106  djudoml  7175  djudomr  7176  uzsinds  10377  fimaxq  10740  ltoddhalfle  11830  phicl2  12146  strsetsid  12427  txdis1cn  12928  xmeter  13086  subctctexmid  13891