Theorem mpanl2 717

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpanl2.1	|- ps
mpanl2.2	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
mpanl2	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mpanl2

Step	Hyp	Ref	Expression
1		mpanl2.1	. . 3 |- ps
2	1	jctr 565	. 2 |- ( ph -> ( ph /\ ps ) )
3		mpanl2.2	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	2, 3	sylan 488	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mpanr1  719  mp3an2  1412  reuss  3908  tfrlem11  7484  tfr3  7495  oe0  7602  dif1en  8193  indpi  9729  map2psrpr  9931  axcnre  9985  muleqadd  10671  divdiv2  10737  addltmul  11268  frnnn0supp  11349  supxrpnf  12148  supxrunb1  12149  supxrunb2  12150  iimulcl  22736  numclwwlkovf2exlem2  27212  eigposi  28695  nmopadjlem  28948  nmopcoadji  28960  opsqrlem6  29004  hstrbi  29125  sgncl  30600  poimirlem3  33412  aacllem  42547