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

Theorem mpanl2 681
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
mpanl2.2
Assertion
Ref Expression
mpanl2

Proof of Theorem mpanl2
StepHypRef Expression
1 mpanl2.1 . . 3
21jctr 542 . 2
3 mpanl2.2 . 2
42, 3sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  mpanr1  683  mp3an2  1312  reuss  3778  tfrlem11  7076  tfr3  7087  oe0  7191  dif1enOLD  7772  dif1en  7773  noinfepOLD  8098  indpi  9306  map2psrpr  9508  axcnre  9562  muleqadd  10218  divdiv2  10281  addltmul  10799  frnnn0supp  10874  supxrpnf  11539  supxrunb1  11540  supxrunb2  11541  iimulcl  21437  numclwwlkovf2ex  25086  eigposi  26755  nmopadjlem  27008  nmopcoadji  27020  opsqrlem6  27064  hstrbi  27185  sgncl  28477  aacllem  33216
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 185  df-an 371
  Copyright terms: Public domain W3C validator