Theorem mpisyl 1467

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  2812  reusv1  4513  iotaexab  5259  fliftcnv  5877  fliftfun  5878  tfrlemibfn  6427  tfr1onlembfn  6443  tfrcllembfn  6456  cnvct  6915  ordiso  7153  exmidomni  7259  djudoml  7347  djudomr  7348  uzsinds  10611  fimaxq  10994  ltoddhalfle  12279  phicl2  12611  strsetsid  12940  txdis1cn  14825  xmeter  14983  2lgslem1  15643  subctctexmid  16078