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  2838  reusv1  4549  iotaexab  5297  fliftcnv  5925  fliftfun  5926  tfrlemibfn  6480  tfr1onlembfn  6496  tfrcllembfn  6509  cnvct  6970  ordiso  7214  exmidomni  7320  djudoml  7412  djudomr  7413  uzsinds  10678  fimaxq  11062  ltoddhalfle  12419  phicl2  12751  strsetsid  13080  txdis1cn  14967  xmeter  15125  2lgslem1  15785  usgredg2v  16037  subctctexmid  16425