Theorem mpisyl 1457

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  2801  reusv1  4494  iotaexab  5238  fliftcnv  5845  fliftfun  5846  tfrlemibfn  6395  tfr1onlembfn  6411  tfrcllembfn  6424  cnvct  6877  ordiso  7111  exmidomni  7217  djudoml  7302  djudomr  7303  uzsinds  10553  fimaxq  10936  ltoddhalfle  12075  phicl2  12407  strsetsid  12736  txdis1cn  14598  xmeter  14756  2lgslem1  15416  subctctexmid  15731