Theorem mpisyl 1465

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  2809  reusv1  4503  iotaexab  5247  fliftcnv  5854  fliftfun  5855  tfrlemibfn  6404  tfr1onlembfn  6420  tfrcllembfn  6433  cnvct  6886  ordiso  7120  exmidomni  7226  djudoml  7313  djudomr  7314  uzsinds  10570  fimaxq  10953  ltoddhalfle  12123  phicl2  12455  strsetsid  12784  txdis1cn  14668  xmeter  14826  2lgslem1  15486  subctctexmid  15801