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  2798  reusv1  4489  iotaexab  5233  fliftcnv  5838  fliftfun  5839  tfrlemibfn  6381  tfr1onlembfn  6397  tfrcllembfn  6410  cnvct  6863  ordiso  7095  exmidomni  7201  djudoml  7279  djudomr  7280  uzsinds  10515  fimaxq  10898  ltoddhalfle  12034  phicl2  12352  strsetsid  12651  txdis1cn  14446  xmeter  14604  subctctexmid  15491