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  4548  iotaexab  5296  fliftcnv  5918  fliftfun  5919  tfrlemibfn  6472  tfr1onlembfn  6488  tfrcllembfn  6501  cnvct  6960  ordiso  7199  exmidomni  7305  djudoml  7397  djudomr  7398  uzsinds  10661  fimaxq  11044  ltoddhalfle  12399  phicl2  12731  strsetsid  13060  txdis1cn  14946  xmeter  15104  2lgslem1  15764  usgredg2v  16016  subctctexmid  16325