Theorem mpisyl 1457

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  2798  reusv1  4490  iotaexab  5234  fliftcnv  5839  fliftfun  5840  tfrlemibfn  6383  tfr1onlembfn  6399  tfrcllembfn  6412  cnvct  6865  ordiso  7097  exmidomni  7203  djudoml  7281  djudomr  7282  uzsinds  10518  fimaxq  10901  ltoddhalfle  12037  phicl2  12355  strsetsid  12654  txdis1cn  14457  xmeter  14615  2lgslem1  15248  subctctexmid  15561