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  3558  tfrlem11  6578  tfr3  6589  oe0  6695  dif1enOLD  7269  dif1en  7270  noinfepOLD  7541  indpi  8710  map2psrpr  8911  axcnre  8965  muleqadd  9591  divdiv2  9651  addltmul  10128  supxrpnf  10822  supxrunb1  10823  supxrunb2  10824  spwpr4  14583  iimulcl  18826  eigposi  23180  nmopadjlem  23433  nmopcoadji  23445  opsqrlem6  23489  hstrbi  23610
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