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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  ceqsex  2860  reusv1  4604  iotaexab  5356  fliftcnv  6001  fliftfun  6002  tfrlemibfn  6599  tfr1onlembfn  6615  tfrcllembfn  6628  cnvct  7097  ssfiexmidt  7180  ordiso  7376  exmidomni  7482  djudoml  7575  djudomr  7576  uzsinds  10881  fimaxq  11270  ltoddhalfle  12660  phicl2  12992  strsetsid  13385  txdis1cn  15379  xmeter  15537  2lgslem1  16210  usgredg2v  16465  1loopgrvd2fi  16546  subctctexmid  17030  wexmiddiffilem  17043  wexmiddifxy  17046