MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpanl2 Unicode version

Theorem mpanl2 663
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
StepHypRef Expression
1 mpanl2.1 . . 3  |-  ps
21jctr 527 . 2  |-  ( ph  ->  ( ph  /\  ps ) )
3 mpanl2.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 458 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpanr1  665  mp3an2  1267  reuss  3614  tfrlem11  6640  tfr3  6651  oe0  6757  dif1enOLD  7331  dif1en  7332  noinfepOLD  7604  indpi  8773  map2psrpr  8974  axcnre  9028  muleqadd  9655  divdiv2  9715  addltmul  10192  supxrpnf  10886  supxrunb1  10887  supxrunb2  10888  spwpr4  14651  iimulcl  18950  eigposi  23327  nmopadjlem  23580  nmopcoadji  23592  opsqrlem6  23636  hstrbi  23757  sibfof  24642
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator