Theorem mpisyl 1423

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  2747  reusv1  4412  fliftcnv  5736  fliftfun  5737  tfrlemibfn  6265  tfr1onlembfn  6281  tfrcllembfn  6294  cnvct  6743  ordiso  6966  exmidomni  7064  djudoml  7133  djudomr  7134  uzsinds  10319  fimaxq  10678  ltoddhalfle  11757  phicl2  12058  strsetsid  12170  txdis1cn  12625  xmeter  12783  subctctexmid  13520