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

Theorem mpanr12 685
Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
Hypotheses
Ref Expression
mpanr12.1
mpanr12.2
mpanr12.3
Assertion
Ref Expression
mpanr12

Proof of Theorem mpanr12
StepHypRef Expression
1 mpanr12.2 . 2
2 mpanr12.1 . . 3
3 mpanr12.3 . . 3
42, 3mpanr1 683 . 2
51, 4mpan2 671 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  2dom  7608  limensuci  7713  phplem4  7719  unfi  7807  fiint  7817  cdaen  8574  isfin1-3  8787  prlem934  9432  0idsr  9495  1idsr  9496  00sr  9497  addresr  9536  mulresr  9537  reclt1  10465  crne0  10554  nominpos  10800  expnass  12273  faclbnd2  12369  crim  12948  sqrlem1  13076  sqrlem7  13082  sqrt00  13097  sqreulem  13192  mulcn2  13418  ege2le3  13825  sin02gt0  13927  opoe  14335  oddprm  14339  pythagtriplem2  14341  pythagtriplem3  14342  pythagtriplem16  14354  pythagtrip  14358  pc1  14379  prmlem0  14591  acsfn0  15057  mgpress  17152  abvneg  17483  pmatcollpw3  19285  leordtval2  19713  txswaphmeo  20306  iccntr  21326  dvlipcn  22395  sinq34lt0t  22902  cosordlem  22918  efif1olem3  22931  basellem3  23356  ppiub  23479  bposlem9  23567  lgsne0  23608  lgsdinn0  23615  chebbnd1  23657  constr1trl  24590  constr2trl  24601  usgrcyclnl2  24641  4cycl4dv  24667  2spontn0vne  24887  eupath2lem3  24979  mayete3i  26646  mayete3iOLD  26647  lnop0  26885  nmcexi  26945  nmoptrii  27013  nmopcoadji  27020  hstle1  27145  hst0  27152  strlem5  27174  jplem1  27187  cnvoprab  27546  lgamgulmlem2  28572  subfacp1lem5  28628  wfisg  29289  frinsg  29325  limsucncmpi  29910  dvasin  30103  fdc  30238  eldioph3b  30698  sinhpcosh  33134
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