Theorem mpisyl 1491

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  2841  reusv1  4555  iotaexab  5305  fliftcnv  5935  fliftfun  5936  tfrlemibfn  6493  tfr1onlembfn  6509  tfrcllembfn  6522  cnvct  6983  ssfiexmidt  7064  ordiso  7234  exmidomni  7340  djudoml  7433  djudomr  7434  uzsinds  10705  fimaxq  11090  ltoddhalfle  12453  phicl2  12785  strsetsid  13114  txdis1cn  15001  xmeter  15159  2lgslem1  15819  usgredg2v  16074  1loopgrvd2fi  16155  subctctexmid  16601