Theorem mpisyl 1496

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  2860  reusv1  4599  iotaexab  5351  fliftcnv  5991  fliftfun  5992  tfrlemibfn  6589  tfr1onlembfn  6605  tfrcllembfn  6618  cnvct  7087  ssfiexmidt  7170  ordiso  7366  exmidomni  7472  djudoml  7565  djudomr  7566  uzsinds  10859  fimaxq  11248  ltoddhalfle  12638  phicl2  12970  strsetsid  13363  txdis1cn  15302  xmeter  15460  2lgslem1  16124  usgredg2v  16379  1loopgrvd2fi  16460  subctctexmid  16944