Theorem mpisyl 1492

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  2842  reusv1  4561  iotaexab  5312  fliftcnv  5946  fliftfun  5947  tfrlemibfn  6537  tfr1onlembfn  6553  tfrcllembfn  6566  cnvct  7027  ssfiexmidt  7108  ordiso  7278  exmidomni  7384  djudoml  7477  djudomr  7478  uzsinds  10752  fimaxq  11137  ltoddhalfle  12517  phicl2  12849  strsetsid  13178  txdis1cn  15072  xmeter  15230  2lgslem1  15893  usgredg2v  16148  1loopgrvd2fi  16229  subctctexmid  16705