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  4606  iotaexab  5359  fliftcnv  6004  fliftfun  6005  tfrlemibfn  6603  tfr1onlembfn  6619  tfrcllembfn  6632  cnvct  7101  ssfiexmidt  7184  ordiso  7382  exmidomni  7488  djudoml  7581  djudomr  7582  uzsinds  10902  fimaxq  11292  ltoddhalfle  12685  phicl2  13021  strsetsid  13443  txdis1cn  15504  xmeter  15662  ppiqub  16293  2lgslem1  16415  usgredg2v  16670  1loopgrvd2fi  16751  subctctexmid  17235  wexmiddiffilem  17248  wexmiddifxy  17251