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

Theorem mpan2 652
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  |-  ps
mpan2.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpan2  |-  ( ph  ->  ch )

Proof of Theorem mpan2
StepHypRef Expression
1 mpan2.1 . . 3  |-  ps
21a1i 10 . 2  |-  ( ph  ->  ps )
3 mpan2.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpdan 649 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpanr12  666  mp3an23  1269  equs4  1964  eueq2  3015  sbcgf  3130  csbconstgf  3170  sbcnestg  3206  csbnestg  3207  csbnest1g  3209  mpteq1  4179  iinexg  4250  nnullss  4314  ord0eln0  4525  eusv2nf  4611  reusv2lem5  4618  eldifpw  4645  ordeleqon  4659  ordsson  4660  ssnlim  4753  xpss1  4874  xpiindi  4900  reldm0  4975  elrnmpt1s  5006  resdm  5072  resid  5085  eliniseg  5121  trinxp  5147  ssrnres  5195  cnveq0  5209  coi2  5268  relrelss  5275  funcnvres  5400  funimaex  5409  fnresin1  5437  fnresin2  5438  fresin  5490  dffv3  5601  ssimaex  5664  dmfco  5673  fvmpt  5682  fvmptnf  5697  fvimacnvALT  5724  dff3  5753  fsn  5776  fsn2  5778  elabrex  5848  f1elima  5871  fliftel1  5893  f1owe  5934  2ndconst  6292  curry1  6294  tposfun  6334  tpostpos2  6339  sorpssuni  6370  sorpssint  6371  riotasv  6436  tfrlem10  6487  tfrlem12  6489  tfr3  6499  seqomlem1  6546  seqomlem2  6547  seqomlem4  6549  abianfplem  6554  ondif2  6585  oa0  6599  om0  6600  oa1suc  6614  om1  6624  oe1  6626  oe1m  6627  omass  6662  oeoalem  6678  oeoelem  6680  nnmsucr  6707  nnm1  6730  nnm2  6731  ecelqsg  6798  xpider  6814  qsel  6822  map0e  6890  fvdiagfn  6897  ixpsnf1o  6941  map1  7024  xp1en  7033  sbthlem7  7062  domunsn  7096  xpmapenlem  7113  infensuc  7124  infi  7171  diffi  7176  dif1enOLD  7177  dif1en  7178  unblem1  7196  unblem2  7197  unblem3  7198  unblem4  7199  isfinite2  7202  infn0  7206  unfilem1  7208  unfilem2  7209  unfir  7212  fofinf1o  7224  fidomdm  7225  cnvfi  7227  pwfilem  7237  mptfi  7242  finsschain  7249  marypha2  7279  inf0  7409  trcl  7497  r1rankidb  7563  snwf  7568  unwf  7569  uniwf  7578  rankval3b  7585  rankr1a  7595  rankxplim3  7638  scott0  7643  card1  7688  pm54.43  7720  infxpenc2  7736  dfac8clem  7746  alephsuc2  7794  alephle  7802  cardaleph  7803  dfacacn  7854  dfac13  7855  dfac12lem2  7857  cdaval  7883  uncdadom  7884  cdaun  7885  cdacomen  7894  cdaassen  7895  cdadom1  7899  cdainf  7905  pwcda1  7907  ackbij1lem18  7950  cflem  7959  cflecard  7966  cfeq0  7969  cfslb  7979  cfsmolem  7983  cfcoflem  7985  cfidm  7988  isfin4-3  8028  fin23lem22  8040  fin23lem12  8044  fin23lem16  8048  fin23lem28  8053  fin23lem38  8062  fin23lem41  8065  fin1a2lem7  8119  fin1a2lem12  8124  fin1a2lem13  8125  hsmexlem8  8137  axcc2lem  8149  axcc3  8151  domtriomlem  8155  axdc3lem2  8164  axdc3lem4  8166  axdc4lem  8168  axcclem  8170  ac6num  8193  ttukeylem4  8226  ttukeylem7  8229  ttukey2g  8230  axdclem  8233  brdom3  8240  brdom5  8241  cardeq0  8261  unsnen  8262  konigthlem  8277  pwcfsdom  8292  canthp1lem1  8361  wunex2  8447  wuncval2  8456  eltsk2g  8460  intgru  8523  ingru  8524  grutsk  8531  axgroth6  8537  mulidpi  8597  nlt1pi  8617  indpi  8618  pinq  8638  mulidnq  8674  1idpr  8740  prlem934  8744  0idsr  8806  1idsr  8807  00sr  8808  negexsr  8811  recexsrlem  8812  sqgt0sr  8815  ax1rid  8870  axcnre  8873  ne0gt0  9012  peano2cn  9071  peano2re  9072  00id  9074  mul02lem2  9076  mul01  9078  subid  9154  subid1  9155  negid  9181  negeq0  9188  peano2rem  9200  lt0neg1  9367  le0neg1  9369  div2neg  9570  recgt0ii  9749  divgt0i2i  9759  ledivp1i  9769  ltdivp1i  9770  peano5nni  9836  peano2nn  9845  nnge1  9859  times2  9933  addltmul  10036  nn0p1nn  10092  peano2nn0  10093  elnnnn0  10096  nn0lele2xi  10105  peano2z  10149  peano2zm  10151  nn0lt10b  10167  suprzcl  10180  zeo  10186  uzindOLD  10195  uzwo  10370  uzwoOLD  10371  uzwo2  10372  infmssuzle  10389  infmssuzcl  10390  rpnnen1lem1  10431  rpnnen1lem3  10433  rpnnen1lem5  10435  rphalfcl  10467  ltpnf  10552  nltmnf  10557  pnfge  10558  nltpnft  10584  qsqueeze  10617  xlt0neg1  10635  xle0neg1  10637  xaddpnf1  10642  xaddmnf1  10644  xaddid1  10655  xsubge0  10670  xmul01  10676  xmulneg1  10678  xmulpnf1  10683  xmulid1  10688  supxrbnd  10736  supxrgtmnf  10737  supxrre1  10738  supxrre2  10739  elioopnf  10826  elicopnf  10828  iccshftri  10859  iccshftli  10861  iccdili  10863  icccntri  10865  fzprval  10933  fzofzp1  11005  fzostep1  11011  flge0nn0  11037  flge1nn  11038  btwnzge0  11042  modfrac  11073  om2uzsuci  11100  axdc4uzlem  11133  ser1const  11191  exp0  11198  exp1  11199  expn1  11203  expubnd  11252  sqval  11253  sqeq0  11258  resqcl  11261  zsqcl  11264  binom21  11309  expnbnd  11320  nn0opthlem2  11374  facnn2  11387  faclbnd4lem3  11398  faclbnd5  11401  bcnn  11414  bcn2  11421  hasheq0  11443  hashsng  11446  hashdif  11465  hashxplem  11475  hashf1lem2  11484  iswrd  11505  wrdval  11506  ccatval2  11522  ccatrid  11525  s111  11538  shftfib  11657  reim0  11693  imval2  11726  cjne0  11738  abssq  11881  max0add  11885  abs2dif  11906  rddif  11914  absrdbnd  11915  rexuz3  11922  rlimdm  12115  isershft  12227  isercolllem2  12229  isercoll  12231  fsum  12284  fsumadd  12302  bcxmas  12385  infcvgaux2i  12407  efi4p  12508  resin4p  12509  recos4p  12510  sinbnd  12551  cosbnd  12552  znnenlem  12581  rpnnen2lem8  12591  rpnnen2  12595  cnso  12616  dvdsmul2  12642  dvdslelem  12664  odd2np1lem  12677  divalglem0  12683  divalglem1  12684  divalglem4  12686  divalglem5  12687  divalglem8  12690  bits0  12710  bitsp1o  12715  bitsf1  12728  sadadd2lem2  12732  gcd1  12802  gcdmultiple  12820  isprm3  12858  phiprm  12936  pc0  12998  pcdvdstr  13019  vdwlem2  13120  vdwlem6  13124  vdwlem8  13126  hashbc0  13143  setsval  13263  setsres  13265  ressinbas  13295  ressress  13296  elrestr  13426  pwssnf1o  13490  xpsfrnel  13558  ismred2  13598  submre  13600  mreacs  13653  oppchomfval  13710  oppcbas  13714  brssc  13784  isssc  13790  yonedalem4c  14144  isprs  14157  lubid  14209  oduleval  14328  oduclatb  14341  gsumval2a  14552  mulg1  14667  mulgnegnn  14670  isghm  14776  cntrnsg  14910  oppgplusfval  14914  efgrelexlemb  15152  frgp0  15162  frgpmhm  15167  vrgpf  15170  cygctb  15271  dprd0  15359  dprd2da  15370  mgpplusg  15422  opprmulfval  15500  subrgint  15660  lsp0  15859  sralem  16023  zcyg  16545  mulgrhm2  16561  zlmsca  16575  chrnzr  16584  ocvz  16678  cssincl  16688  css0  16689  css1  16690  0opn  16750  topopn  16752  basdif0  16791  tgval  16793  unitg  16805  tgdif0  16830  isopn2  16869  0cld  16875  ntropn  16886  ntrval2  16888  ntrdif  16889  clsdif  16890  cmclsopn  16899  cmntrcld  16900  clstop  16906  ntrtop  16907  cls0  16917  ntr0  16918  mretopd  16929  neips  16950  maxlp  16978  isperf2  16983  rest0  17000  iocpnfordt  17045  icomnfordt  17046  mnfnei  17051  1stckgen  17349  ptbasfi  17376  pthaus  17432  fbssfi  17628  isfil2  17647  ssfg  17663  filcon  17674  fbasrn  17675  filufint  17711  imaelfm  17742  fmfnfmlem4  17748  fclsfnflim  17818  alexsubALTlem3  17839  alexsubALTlem4  17840  xmetres  18024  metres  18025  mopnex  18161  prdsms  18173  tngds  18260  nmoge0  18326  cnfldnm  18384  tgioo  18398  xrtgioo  18408  xrsmopn  18414  negcncf  18519  phtpy01  18581  pco0  18610  tchtopn  18755  tchnmfval  18757  caussi  18821  minveclem3b  18890  ovolfioo  18925  ovolficc  18926  ovolfsf  18929  ovolctb  18947  ovolctb2  18949  ovolfiniun  18958  ovoliun2  18963  ovolshftlem1  18966  ovolscalem1  18970  ovolicopnf  18981  iunmbl2  19012  uniioombllem2  19036  opnmblALT  19056  ismbf  19083  mbfinf  19118  0plef  19125  itg1climres  19167  itg2cnlem1  19214  iblitg  19221  ibl0  19239  itgcn  19295  cnlimc  19336  dvfre  19398  dvnfre  19399  dveflem  19424  dvef  19425  dvlipcn  19439  lhop2  19460  itgsubstlem  19493  evl1rhm  19510  ply1rem  19647  coefv0  19727  plyrecj  19758  vieta1lem2  19789  aannenlem1  19806  aaliou2b  19819  ulmval  19857  ulmpm  19860  ulmdvlem1  19877  mtest  19881  efcn  19920  sin2pim  19954  cos2pim  19955  sinmpi  19956  cosmpi  19957  sinppi  19958  cosppi  19959  efimpi  19960  sincosq1lem  19966  sincosq2sgn  19968  sincosq3sgn  19969  sincosq4sgn  19970  sinq12gt0  19976  sinq34lt0t  19978  sincosq1eq  19981  abssinper  19987  efif1o  20009  relogcn  20090  ellogdm  20091  efopn  20110  cxp0  20122  cxp1  20123  cxpsqr  20155  logsqr  20156  atandm3  20279  atanbnd  20327  atancn  20337  leibpi  20343  efrlim  20369  logdifbnd  20393  vmaprm  20461  ppip1le  20505  ppieq0  20520  prmorcht  20522  ppiublem1  20547  ppiub  20549  chpeq0  20553  chtub  20557  fsumvma  20558  pclogsum  20560  chpval2  20563  dchrresb  20604  dchrptlem1  20609  lgs0  20654  lgs2  20658  lgsdir2lem2  20669  lgsdir2lem4  20671  lgsdchrval  20692  lgsdchr  20693  lgseisenlem2  20695  dirith2  20783  selberg2lem  20805  qabvle  20880  qabvexp  20881  ostth  20894  ex-po  20928  gx1  21035  addinv  21125  vcoprne  21243  nvnd  21365  ipval2lem3  21386  ipval2  21388  ipval2lem6  21392  4ipval3  21393  ipidsq  21394  dipcj  21398  dip0r  21401  nmlnogt0  21483  blocni  21491  ipasslem2  21518  ipasslem8  21523  ipasslem9  21524  ajval  21548  ubthlem1  21557  hvaddid2  21710  hvsub0  21763  hi02  21784  hlimi  21875  isch2  21911  chlimi  21922  chsupunss  22031  shsupunss  22033  chlejb1i  22163  h1dei  22237  h1de2ci  22243  spanunsni  22266  pjoml2i  22272  pjorthi  22356  mayete3i  22415  mayete3iOLD  22416  hosubid1  22486  nmopge0  22599  nmfnge0  22615  adj1  22621  adjeq  22623  lnop0  22654  lnopmi  22688  nmophmi  22719  cnlnadjlem5  22759  cnlnadjeui  22765  unierri  22792  leoprf2  22815  leopnmid  22826  nmopleid  22827  hstles  22919  hst0  22921  strlem3a  22940  dmdbr2  22991  mdsl1i  23009  mdsl2i  23010  mdsl2bi  23011  cvmdi  23012  mdslmd1lem1  23013  mdslmd1lem2  23014  mdslmd1i  23017  mdslmd2i  23018  csmdsymi  23022  mdexchi  23023  superpos  23042  atomli  23070  atordi  23072  chirredlem1  23078  chirredlem2  23079  atcvat4i  23085  atabsi  23089  mdsymlem1  23091  mdsymlem5  23095  mdsymlem6  23096  sumdmdii  23103  dmdbr5ati  23110  dmdbr6ati  23111  mddmdin0i  23119  cdj3lem2  23123  inimasn  23232  xppreima  23259  abfmpunirn  23264  abfmpel  23267  xrdifh  23342  xrge0neqmnf  23404  neiptopnei  23445  xrmulc1cn  23472  rge0scvg  23491  lmxrge0  23493  ustfilxp  23518  ustuqtop1  23545  ustuqtop2  23546  ustuqtop3  23547  ustuqtop4  23548  utopsnneiplem  23551  ucnima  23576  blval2  23608  zrhre  23652  rnlogblem  23665  logb1  23669  esumcst  23721  esumfzf  23725  esumfsupre  23727  hasheuni  23741  sgon  23773  dmvlsiga  23778  sigainb  23785  sigagenid  23800  measval  23818  ismeas  23819  probmeasb  23937  rrvsum  23961  ballotlemfcc  24000  lgamgulmlem2  24063  ptpcon  24168  cvmsss2  24209  cvmlift2lem12  24249  cvmlift2lem13  24250  cvmliftphtlem  24252  cvmliftpht  24253  umgra0  24281  iseupa  24285  relin01  24495  bcnm1  24502  fprod  24568  risefac0  24632  fallfac0  24633  risefac1  24636  fallfac1  24637  fprb  24687  predreseq  24737  predep  24750  trpred0  24797  wfr3g  24813  wfrlem14  24827  wfrlem15  24828  frr3g  24838  noxpsgn  24877  elfix  25001  dffix2  25003  funpartfv  25042  altopeq1  25056  brbtwn  25086  colinearalglem4  25096  axlowdimlem13  25141  axlowdimlem17  25145  brcolinear2  25240  bpoly2  25351  bpoly3  25352  bpoly4  25353  fsumcube  25354  ontgval  25429  onint1  25447  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  itg2gt0cn  25495  itgaddnclem2  25499  gtinf  25558  cldbnd  25568  ivthALT  25582  refref  25609  refssfne  25618  finptfin  25621  tailfb  25650  unirep  25673  sdclem2  25776  sstotbnd3  25823  totbndbnd  25836  heibor1lem  25856  heiborlem7  25864  bfplem1  25869  prnc  26015  fninfp  26077  fndifnfp  26079  fnnfpeq0  26081  ralxpmap  26084  mapfzcons1cl  26118  eldioph3b  26167  eldiophss  26177  0dioph  26181  vdioph  26182  eldioph4b  26217  eldioph4i  26218  rencldnfilem  26226  rmxy1  26330  rmxy0  26331  rmxm1  26342  rmym1  26343  monotoddzzfi  26350  nn0sqcl  26399  aomclem6  26479  pwslnmlem0  26516  pwslnmlem1  26517  isnumbasabl  26594  psgneldm2i  26751  seff  26861  lhe4.4ex1a  26869  fmuldfeqlem1  27035  stoweidlem22  27094  stoweidlem41  27113  stoweidlem59  27131  rlimdmafv  27365  finresfin  27448  injresinj  27460  bcn2p1  27463  hash2pr  27469  hash2prde  27470  umisuhgra  27506  uhgra0  27508  usisuslgra  27534  usgra0  27537  usgraedg4  27552  usgrafisbase  27574  uvtx01vtx  27638  fargshiftlem  27740  usgrcyclnl2  27748  constr3trl  27766  constr3pth  27767  constr3cycl  27768  4cycl4dv  27774  frgrancvvdeqlemA  27853  eelT0  28293  snssl  28350  bnj535  28667  bnj580  28690  bnj907  28742  bnj1253  28792  equs4NEW7  28937  lub0N  29431  glb0N  29435  glbconN  29618  atpointN  29984  polsubN  30148  pol0N  30150  pol1N  30151  2polvalN  30155  2polssN  30156  3polN  30157  pcl0N  30163  2pmaplubN  30167  pnonsingN  30174  polsubclN  30193  cdleme31snd  30627  cdlemefs32sn1aw  30655  cdleme43fsv1snlem  30661  cdleme41sn3a  30674  cdleme32a  30682  cdleme40m  30708  cdleme40n  30709  cdleme42b  30719  istendo  31001  cdlemk40  31158  cdlemkid  31177  dihvalcqpre  31477
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 177  df-an 360
  Copyright terms: Public domain W3C validator