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

Theorem mpanl12 682
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mpanl12.1
mpanl12.2
mpanl12.3
Assertion
Ref Expression
mpanl12

Proof of Theorem mpanl12
StepHypRef Expression
1 mpanl12.2 . 2
2 mpanl12.1 . . 3
3 mpanl12.3 . . 3
42, 3mpanl1 680 . 2
51, 4mpan 670 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  reuun1  3779  frminex  4864  opthreg  8056  unsnen  8949  axcnre  9562  addgt0  10063  addgegt0  10064  addgtge0  10065  addge0  10066  addgt0i  10117  addge0i  10118  addgegt0i  10119  add20i  10121  mulge0i  10125  recextlem1  10204  recne0  10245  recdiv  10275  rec11i  10310  recgt1  10466  prodgt0i  10477  prodge0i  10478  xadddi2  11518  iccshftri  11684  iccshftli  11686  iccdili  11688  icccntri  11690  mulexpz  12206  expaddz  12210  iexpcyc  12272  cnpart  13073  resqrex  13084  sqreulem  13192  amgm2  13202  rlim  13318  ello12  13339  elo12  13350  efcllem  13813  ege2le3  13825  dvdslelem  14030  divalglem1  14052  divalglem6  14056  divalglem9  14059  gcdaddmlem  14166  sqnprm  14239  prmlem1  14593  prmlem2  14605  xpscfn  14956  m1expaddsub  16523  psgnuni  16524  gzrngunitlem  18482  lmres  19801  zdis  21321  iihalf1  21431  lmclimf  21742  vitali  22022  ismbf  22037  ismbfcn  22038  mbfconst  22042  cncombf  22065  cnmbf  22066  limcfval  22276  dvnfre  22355  quotlem  22696  ulmval  22775  ulmpm  22778  abelthlem2  22827  abelthlem3  22828  abelthlem5  22830  abelthlem7  22833  efcvx  22844  logtayl  23041  logccv  23044  cxpcn3  23122  emcllem2  23326  basellem5  23358  bposlem7  23565  chebbnd1lem3  23656  dchrisumlem3  23676  iscgrgd  23905  axcontlem2  24268  nv1  25579  blocnilem  25719  ipasslem8  25752  siii  25768  ubthlem1  25786  norm1  26167  hhshsslem2  26184  hoscli  26681  hodcli  26682  cnlnadjlem7  26992  adjbdln  27002  pjnmopi  27067  strlem1  27169  rexdiv  27622  tpr2rico  27894  qqhre  27998  signsply0  28508  zetacvg  28557  subfacval3  28633  erdszelem4  28638  erdszelem8  28642  m1expevenALT  28663  elmrsubrn  28880  rdgprc  29227  tz6.26i  29286  wfii  29288  frindi  29324  ismblfin  30055  itg2addnclem  30066  caures  30253
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