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  6604  tfr1onlembfn  6620  tfrcllembfn  6633  cnvct  7103  ssfiexmidt  7186  ordiso  7382  exmidomni  7488  djudoml  7581  djudomr  7582  uzsinds  10901  fimaxq  11291  ltoddhalfle  12684  phicl2  13020  strsetsid  13442  txdis1cn  15521  xmeter  15679  ppiqub  16310  2lgslem1  16432  usgredg2v  16687  1loopgrvd2fi  16768  subctctexmid  17252  wexmiddiffilem  17265  wexmiddifxy  17268