Theorem mpisyl 1423

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  2727  reusv1  4387  fliftcnv  5704  fliftfun  5705  tfrlemibfn  6233  tfr1onlembfn  6249  tfrcllembfn  6262  cnvct  6711  ordiso  6929  exmidomni  7022  djudoml  7092  djudomr  7093  uzsinds  10246  fimaxq  10605  ltoddhalfle  11626  phicl2  11926  strsetsid  12031  txdis1cn  12486  xmeter  12644  subctctexmid  13369