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

Theorem mpan2 671
Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpan2.1
mpan2.2
Assertion
Ref Expression
mpan2

Proof of Theorem mpan2
StepHypRef Expression
1 mpan2.1 . . 3
21a1i 11 . 2
3 mpan2.2 . 2
42, 3mpdan 668 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  mpanr12  685  mp3an23  1316  eueq2  3273  sbcgf  3399  sbcralg  3411  csbconstgf  3446  sbcnestg  3841  csbnestg  3842  csbnest1g  3845  mpteq1  4532  iinexg  4612  eusv2nf  4650  reusv2lem5  4657  nnullss  4714  ord0eln0  4937  xpss1  5116  xpiindi  5143  reldm0  5225  elrnmpt1s  5255  resdm  5320  resid  5336  eliniseg  5371  trinxp  5397  inimasn  5428  ssrnres  5450  cnveq0  5468  coi2  5529  relrelss  5536  funcnvres  5662  funimaex  5671  fnresin1  5700  fnresin2  5701  fresin  5759  dffv3  5867  ssimaex  5938  dmfco  5947  fvmpt  5956  fvmptnf  5973  fvimacnvALT  6006  dff3  6044  fsn  6069  fsn2  6071  fvrnressn  6086  fninfp  6098  fndifnfp  6100  fnnfpeq0  6102  elabrex  6155  f1elima  6171  fliftel1  6208  f1owe  6249  sorpssuni  6589  sorpssint  6590  eldifpw  6612  ordeleqon  6624  ordsson  6625  ssnlim  6718  2ndconst  6889  curry1  6892  tposfun  6990  tpostpos2  6995  tfrlem10  7075  tfrlem12  7077  tfr3  7087  seqomlem1  7134  seqomlem2  7135  seqomlem4  7137  ondif2  7171  oa0  7185  om0  7186  oa1suc  7200  om1  7210  oe1  7212  oe1m  7213  omass  7248  oeoalem  7264  oeoelem  7266  nnmsucr  7293  nnm1  7316  nnm2  7317  ecelqsg  7385  xpider  7401  qsel  7409  map0e  7476  fvdiagfn  7483  ralxpmap  7488  ixpsnf1o  7529  map1  7614  xp1en  7623  sbthlem7  7653  domunsn  7687  xpmapenlem  7704  infensuc  7715  infi  7763  finresfin  7765  diffi  7771  dif1enOLD  7772  dif1en  7773  findcard2d  7782  unblem1  7792  unblem2  7793  unblem3  7794  unblem4  7795  isfinite2  7798  infn0  7802  unfilem1  7804  unfilem2  7805  unfir  7808  fofinf1o  7821  cnvfi  7824  pwfilem  7834  mptfi  7839  finsschain  7847  marypha2  7919  inf0  8059  trcl  8180  r1rankidb  8243  snwf  8248  unwf  8249  uniwf  8258  rankval3b  8265  rankr1a  8275  rankxplim3  8320  scott0  8325  card1  8370  pm54.43  8402  infxpenc2  8420  infxpenc2OLD  8424  dfac8clem  8434  alephsuc2  8482  alephle  8490  cardaleph  8491  dfacacn  8542  dfac13  8543  dfac12lem2  8545  cdaval  8571  uncdadom  8572  cdaun  8573  cdacomen  8582  cdaassen  8583  cdadom1  8587  cdainf  8593  pwcda1  8595  ackbij1lem18  8638  cflem  8647  cflecard  8654  cfeq0  8657  cfslb  8667  cfsmolem  8671  cfcoflem  8673  cfidm  8676  isfin4-3  8716  fin23lem12  8732  fin23lem16  8736  fin23lem28  8741  fin23lem38  8750  fin23lem41  8753  fin1a2lem7  8807  fin1a2lem12  8812  fin1a2lem13  8813  hsmexlem8  8825  axcc2lem  8837  axcc3  8839  domtriomlem  8843  axdc3lem2  8852  axdc3lem4  8854  axdc4lem  8856  axcclem  8858  ac6num  8880  ttukeylem4  8913  ttukeylem7  8916  ttukey2g  8917  axdclem  8920  brdom3  8927  brdom5  8928  cardeq0  8948  unsnen  8949  konigthlem  8964  pwcfsdom  8979  canthp1lem1  9051  wunex2  9137  wuncval2  9146  eltsk2g  9150  intgru  9213  ingru  9214  grutsk  9221  axgroth6  9227  mulidpi  9285  nlt1pi  9305  indpi  9306  pinq  9326  mulidnq  9362  1idpr  9428  prlem934  9432  0idsr  9495  1idsr  9496  00sr  9497  negexsr  9500  recexsrlem  9501  sqgt0sr  9504  ax1rid  9559  axcnre  9562  ne0gt0  9710  peano2cn  9773  peano2re  9774  00id  9776  mul02lem2  9778  mul01  9780  subid  9861  subid1  9862  negid  9889  negeq0  9896  peano2cnm  9908  peano2rem  9909  lt0neg1  10083  le0neg1  10085  relin01  10102  div2neg  10292  recgt0ii  10476  divgt0i2i  10486  ledivp1i  10496  ltdivp1i  10497  peano5nni  10564  peano2nn  10573  nnge1  10587  times2  10680  addltmul  10799  nn0p1nn  10860  peano2nn0  10861  nn0lele2xi  10873  frnnn0fsupp  10876  peano2z  10930  peano2zm  10932  nn0lt10bOLD  10951  suprzcl  10967  zeo  10973  uzindOLD  10982  uzwo  11173  uzwoOLD  11174  uzwo2  11175  infmssuzle  11193  infmssuzcl  11194  rpnnen1lem1  11237  rpnnen1lem3  11239  rpnnen1lem5  11241  rphalfcl  11273  ltpnf  11360  nltmnf  11367  pnfge  11368  nltpnft  11396  qsqueeze  11429  xlt0neg1  11447  xle0neg1  11449  xaddpnf1  11454  xaddmnf1  11456  xaddid1  11467  xsubge0  11482  xmul01  11488  xmulneg1  11490  xmulpnf1  11495  xmulid1  11500  supxrbnd  11549  supxrgtmnf  11550  supxrre1  11551  supxrre2  11552  elioopnf  11647  elicopnf  11649  iccshftri  11684  iccshftli  11686  iccdili  11688  icccntri  11690  fzprval  11769  fzofzp1  11909  fzostep1  11922  injresinj  11926  flge0nn0  11954  flge1nn  11955  btwnzge0  11961  modfrac  12009  om2uzsuci  12059  axdc4uzlem  12092  ser1const  12163  exp0  12170  exp1  12172  expn1  12176  nn0sqcl  12193  expubnd  12226  sqval  12227  sqeq0  12232  resqcl  12235  zsqcl  12238  binom21  12284  expnbnd  12295  nn0opthlem2  12349  bcnn  12390  bcn2  12397  bcn2p1  12403  hasheq0  12433  hashsng  12438  hashen1  12439  hashdif  12476  hashxplem  12491  hashf1lem2  12505  hash2pr  12515  hash2prde  12516  pr2pwpr  12520  hash3tr  12529  iswrd  12550  wrdval  12551  ccatval2  12596  ccatrid  12604  lswccat0lsw  12608  s111  12623  swrd0len0  12660  repsw0  12749  repsw1  12755  cshw0  12765  wwlktovf  12894  shftfib  12905  reim0  12951  imval2  12984  cjne0  12996  abssq  13139  max0add  13143  abs2dif  13165  rddif  13173  absrdbnd  13174  rexuz3  13181  rlimdm  13374  isershft  13486  isercolllem2  13488  isercoll  13490  fsum  13542  fsumadd  13561  fsumsplitsnun  13570  bcxmas  13647  infcvgaux2i  13669  fprod  13748  efi4p  13872  resin4p  13873  recos4p  13874  sinbnd  13915  cosbnd  13916  znnenlem  13945  rpnnen2lem8  13955  rpnnen2  13959  cnso  13980  dvdsmul2  14006  dvdslelem  14030  odd2np1lem  14045  divalglem0  14051  divalglem1  14052  divalglem4  14054  divalglem5  14055  divalglem8  14058  bits0  14078  bitsp1o  14083  bitsf1  14096  sadadd2lem2  14100  gcd1  14170  gcdmultiple  14188  phiprm  14307  pc0  14378  pcdvdstr  14399  vdwlem2  14500  vdwlem6  14504  vdwlem8  14506  hashbc0  14523  setsval  14656  fsets  14658  setsres  14660  ressinbas  14693  ressress  14694  elrestr  14826  pwssnf1o  14895  xpsfrnel  14960  ismred2  15000  submre  15002  mreacs  15055  oppchomfval  15109  brssc  15183  isssc  15189  yonedalem4c  15546  isprs  15559  oduleval  15761  oduclatb  15774  gsumval2a  15906  mulg1  16149  mulgnegnn  16152  isghm  16267  cntrnsg  16379  oppgplusfval  16383  psgneldm2i  16530  efgrelexlemb  16768  frgp0  16778  frgpmhm  16783  vrgpf  16786  cygctb  16894  dprd0  17078  dprd2da  17091  mgpplusg  17145  opprmulfval  17274  subrgint  17451  lsp0  17655  sralem  17823  rlmval2  17840  fczpsrbag  18016  mplvalOLD  18085  ply1idvr1  18334  evls1rhmlem  18358  evl1fval1lem  18366  zringcyg  18513  zcyg  18518  mulgrhm2  18533  mulgrhm2OLD  18536  zlmsca  18558  chrnzr  18567  zrhpsgnelbas  18630  ocvz  18709  cssincl  18719  css0  18720  css1  18721  frlmip  18809  mat1scmat  19041  marrepeval  19065  decpmatid  19271  0opn  19413  topopn  19415  basdif0  19454  tgval  19456  unitgOLD  19469  isopn2  19533  0cld  19539  ntropn  19550  ntrval2  19552  ntrdif  19553  clsdif  19554  cmclsopn  19563  cmntrcld  19564  clstop  19570  ntrtop  19571  cls0  19581  ntr0  19582  mretopd  19593  neips  19614  neiptopnei  19633  maxlp  19648  isperf2  19653  rest0  19670  iocpnfordt  19716  icomnfordt  19717  mnfnei  19722  bwthOLD  19911  refref  20014  unisngl  20028  1stckgen  20055  ptbasfi  20082  pthaus  20139  imasnopn  20191  imasncld  20192  imasncls  20193  fbssfi  20338  isfil2  20357  ssfg  20373  filcon  20384  fbasrn  20385  filufint  20421  imaelfm  20452  fmfnfmlem4  20458  fclsfnflim  20528  alexsubALTlem3  20549  alexsubALTlem4  20550  ustfilxp  20715  ustuqtop1  20744  ustuqtop2  20745  ustuqtop3  20746  ustuqtop4  20747  utopsnneiplem  20750  utopsnnei  20752  utop2nei  20753  cfiluweak  20798  neipcfilu  20799  xmetres  20867  metres  20868  mopnex  21022  prdsms  21034  blval2  21078  metucnOLD  21091  metucn  21092  tngds  21162  nmoge0  21228  cnfldnm  21286  tgioo  21301  xrtgioo  21311  xrsmopn  21317  negcncf  21422  phtpy01  21485  pco0  21514  tchtopn  21669  tchnmfval  21671  caussi  21736  rrxip  21822  minveclem3b  21843  ovolfioo  21879  ovolficc  21880  ovolfsf  21883  ovolctb  21901  ovolctb2  21903  ovolfiniun  21912  ovoliun2  21917  ovolshftlem1  21920  ovolscalem1  21924  ovolicopnf  21935  iunmbl2  21967  uniioombllem2  21992  opnmblALT  22012  ismbf  22037  mbfinf  22072  0plef  22079  itg1climres  22121  itg2cnlem1  22168  iblitg  22175  ibl0  22193  itgcn  22249  cnlimc  22292  dvfre  22354  dvnfre  22355  dveflem  22380  dvef  22381  dvlipcn  22395  lhop2  22416  itgsubstlem  22449  mdegfvalOLD  22461  deg1val  22496  ply1rem  22564  coefv0  22645  plyrecj  22676  vieta1lem2  22707  aannenlem1  22724  aaliou2b  22737  ulmval  22775  ulmpm  22778  ulmdvlem1  22795  mtest  22799  efcn  22838  sin2pim  22878  cos2pim  22879  sinmpi  22880  cosmpi  22881  sinppi  22882  cosppi  22883  efimpi  22884  sincosq1lem  22890  sincosq2sgn  22892  sincosq3sgn  22893  sincosq4sgn  22894  sinq12gt0  22900  sinq34lt0t  22902  sincosq1eq  22905  abssinper  22911  efif1o  22933  relogcn  23019  ellogdm  23020  efopn  23039  cxp0  23051  cxp1  23052  cxpsqrt  23084  logsqrt  23085  atandm3  23209  atanbnd  23257  atancn  23267  leibpi  23273  efrlim  23299  logdifbnd  23323  vmaprm  23391  ppip1le  23435  ppieq0  23450  prmorcht  23452  ppiublem1  23477  ppiub  23479  chpeq0  23483  chtub  23487  fsumvma  23488  pclogsum  23490  chpval2  23493  dchrresb  23534  dchrptlem1  23539  lgs0  23584  lgs2  23588  lgsdir2lem2  23599  lgsdir2lem4  23601  lgsdchrval  23622  lgsdchr  23623  lgseisenlem2  23625  dirith2  23713  selberg2lem  23735  qabvle  23810  qabvexp  23811  ostth  23824  istrkg2ld  23858  ttgval  24178  cchhllem  24190  brbtwn  24202  colinearalglem4  24212  uhgra0  24309  umgra0  24325  umisuhgra  24327  uslisushgra  24363  usisuslgra  24365  usgra0  24370  usgraedg4  24387  usgrafisbase  24414  usgrasscusgra  24483  uvtx01vtx  24492  usgra2adedgwlkonALT  24616  usgra2wlkspthlem2  24620  fargshiftlem  24634  usgrcyclnl2  24641  constr3trl  24659  constr3pth  24660  constr3cycl  24661  4cycl4dv  24667  wwlkn0s  24705  el2wlkonotlem  24862  usg2wlkonot  24883  usg2wotspth  24884  iseupa  24965  frgrancvvdeqlemA  25037  ex-po  25156  gx1  25264  addinv  25354  vcoprne  25472  nvnd  25594  ipval2lem3  25615  ipval2  25617  ipval2lem6  25621  4ipval3  25622  ipidsq  25623  dipcj  25627  dip0r  25630  nmlnogt0  25712  blocni  25720  ipasslem2  25747  ipasslem8  25752  ipasslem9  25753  ajval  25777  ubthlem1  25786  hvaddid2  25940  hvsub0  25993  hi02  26014  hlimi  26105  isch2  26141  chlimi  26152  chsupunss  26262  shsupunss  26264  chlejb1i  26394  h1dei  26468  h1de2ci  26474  spanunsni  26497  pjoml2i  26503  pjorthi  26587  mayete3i  26646  mayete3iOLD  26647  hosubid1  26717  nmopge0  26830  nmfnge0  26846  adj1  26852  adjeq  26854  lnop0  26885  lnopmi  26919  nmophmi  26950  cnlnadjlem5  26990  cnlnadjeui  26996  unierri  27023  leoprf2  27046  leopnmid  27057  nmopleid  27058  hstles  27150  hst0  27152  strlem3a  27171  dmdbr2  27222  mdsl1i  27240  mdsl2i  27241  mdsl2bi  27242  cvmdi  27243  mdslmd1lem1  27244  mdslmd1lem2  27245  mdslmd1i  27248  mdslmd2i  27249  csmdsymi  27253  mdexchi  27254  superpos  27273  atomli  27301  atordi  27303  chirredlem1  27309  chirredlem2  27310  atcvat4i  27316  atabsi  27320  mdsymlem1  27322  mdsymlem5  27326  mdsymlem6  27327  sumdmdii  27334  dmdbr5ati  27341  dmdbr6ati  27342  mddmdin0i  27350  cdj3lem2  27354  xppreima  27487  abfmpunirn  27490  abfmpel  27493  fgreu  27513  fpwrelmapffslem  27555  fpwrelmap  27556  xlemnf  27571  xrge0infss  27580  xrdifh  27591  clatp0cl  27659  clatp1cl  27660  xrge0neqmnf  27679  resvval  27817  rearchi  27832  locfinreflem  27843  locfinref  27844  ordtconlem1  27906  rge0scvg  27931  lmxrge0  27934  qqh0  27965  qqh1  27966  zrhre  27997  rnlogblem  28015  logb1  28019  esumcst  28071  esumfzf  28075  esumfsupre  28077  hasheuni  28091  sgon  28124  dmvlsiga  28129  sigainb  28136  measval  28169  ismeas  28170  sxbrsigalem0  28242  eulerpartlemmf  28314  eulerpartlemgs2  28319  eulerpartlemn  28320  rrvsum  28393  ballotlem2  28427  ballotlemfcc  28432  ballotlem4  28437  signsplypnf  28507  signsply0  28508  signsw0glem  28510  signswrid  28515  signlem0  28544  ptpcon  28678  cvmsss2  28719  cvmlift2lem12  28759  cvmlift2lem13  28760  cvmliftphtlem  28762  cvmliftpht  28763  mppsthm  28939  bcnm1  29109  risefac0  29149  fallfac0  29150  risefac1  29155  fallfac1  29156  fprb  29203  opelco3  29208  predreseq  29259  predep  29272  trpred0  29319  wfr3g  29342  wfrlem14  29356  wfrlem15  29357  wlimeq1  29376  frr3g  29386  noxpsgn  29425  funpartfv  29595  imagesset  29603  altopeq1  29613  brcolinear2  29708  bpoly2  29819  bpoly3  29820  bpoly4  29821  fsumcube  29822  ontgval  29896  onint1  29914  finixpnum  30038  tan2h  30047  ptrest  30048  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  ftc1anclem5  30094  ftc1anclem8  30097  dvasin  30103  dvacos  30104  gtinf  30137  cldbnd  30144  ivthALT  30153  refssfne  30176  tailfb  30195  sdclem2  30235  totbndbnd  30285  heibor1lem  30305  heiborlem7  30313  bfplem1  30318  prnc  30464  mapfzcons1cl  30650  eldioph3b  30698  eldiophss  30708  0dioph  30712  vdioph  30713  eldioph4b  30745  eldioph4i  30746  rencldnfilem  30754  rmxy1  30858  rmxy0  30859  rmxm1  30870  rmym1  30871  monotoddzzfi  30878  aomclem6  31005  pwslnmlem0  31037  pwslnmlem1  31038  isnumbasabl  31055  areaquad  31184  seff  31189  lcm0val  31200  dvdslcm  31204  lcmeq0  31206  lcmgcd  31213  lhe4.4ex1a  31234  elabrexg  31430  fmuldfeqlem1  31576  fmuldfeq  31577  infrglb  31584  climneg  31616  sumnnodd  31636  addccncf2  31678  dvsinax  31708  stoweidlem18  31800  stoweidlem19  31801  stoweidlem22  31804  stoweidlem34  31816  stoweidlem40  31822  stoweidlem41  31823  stoweidlem55  31837  stoweidlem59  31841  dirker2re  31874  dirkerdenne0  31875  fourierdlem48  31937  fourierdlem49  31938  fourierdlem70  31959  fourierdlem71  31960  fourierdlem104  31993  fourierdlem112  32001  fouriersw  32014  etransclem46  32063  etransclem48  32065  rlimdmafv  32262  fsummmodsnunz  32348  usgra2pthspth  32351  usgra2pthlem1  32353  2zrngnmlid  32755  2zrngnmrid  32756  mpt2exxg2  32927  lco0  33028  zlmodzxzldeplem3  33103  aacllem  33216  eelT0  33572  snssl  33630  sineq0ALT  33737  bnj535  33948  bnj580  33971  bnj907  34023  bnj1253  34073  bj-inftyexpiinv  34611  bj-inftyexpidisj  34613  riotasv  34690  glbconN  35101  atpointN  35467  polsubN  35631  pol0N  35633  pol1N  35634  2polvalN  35638  2polssN  35639  3polN  35640  pcl0N  35646  2pmaplubN  35650  pnonsingN  35657  polsubclN  35676  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdleme41sn3a  36159  cdleme32a  36167  cdleme40m  36193  cdleme40n  36194  cdleme42b  36204  istendo  36486  cdlemk40  36643  cdlemkid  36662  dihvalcqpre  36962  taupilem1  37696  heeq1  37801
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