Theorem mpisyl 1492

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  2852  reusv1  4579  iotaexab  5331  fliftcnv  5968  fliftfun  5969  tfrlemibfn  6559  tfr1onlembfn  6575  tfrcllembfn  6588  cnvct  7050  ssfiexmidt  7133  ordiso  7327  exmidomni  7433  djudoml  7526  djudomr  7527  uzsinds  10806  fimaxq  11194  ltoddhalfle  12579  phicl2  12911  strsetsid  13245  txdis1cn  15143  xmeter  15301  2lgslem1  15964  usgredg2v  16219  1loopgrvd2fi  16300  subctctexmid  16774