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  1901  eueq2  2941  sbcgf  3056  csbconstgf  3096  sbcnestg  3132  csbnestg  3133  csbnest1g  3135  mpteq1  4102  iinexg  4173  nnullss  4237  ord0eln0  4448  eusv2nf  4534  reusv2lem5  4541  eldifpw  4568  ordeleqon  4582  ordsson  4583  ssnlim  4676  xpss1  4797  xpiindi  4823  reldm0  4898  elrnmpt1s  4929  resdm  4995  resid  5008  eliniseg  5044  trinxp  5070  ssrnres  5118  cnveq0  5132  coi2  5191  relrelss  5198  funcnvres  5323  funimaex  5332  fnresin1  5360  fnresin2  5361  fresin  5412  dffv3  5523  ssimaex  5586  dmfco  5595  fvmpt  5604  fvmptnf  5619  fvimacnvALT  5646  dff3  5675  fsn  5698  fsn2  5700  elabrex  5767  f1elima  5789  fliftel1  5811  f1owe  5852  2ndconst  6210  curry1  6212  tposfun  6252  tpostpos2  6257  sorpssuni  6288  sorpssint  6289  riotasv  6354  tfrlem10  6405  tfrlem12  6407  tfr3  6417  seqomlem1  6464  seqomlem2  6465  seqomlem4  6467  abianfplem  6472  ondif2  6503  oa0  6517  om0  6518  oa1suc  6532  om1  6542  oe1  6544  oe1m  6545  omass  6580  oeoalem  6596  oeoelem  6598  nnmsucr  6625  nnm1  6648  nnm2  6649  ecelqsg  6716  xpider  6732  qsel  6740  map0e  6807  fvdiagfn  6814  ixpsnf1o  6858  map1  6941  xp1en  6950  sbthlem7  6979  domunsn  7013  xpmapenlem  7030  infensuc  7041  diffi  7091  dif1enOLD  7092  dif1en  7093  unblem1  7111  unblem2  7112  unblem3  7113  unblem4  7114  isfinite2  7117  infn0  7121  unfilem1  7123  unfilem2  7124  unfir  7127  fofinf1o  7139  fidomdm  7140  cnvfi  7142  pwfilem  7152  mptfi  7157  finsschain  7164  marypha2  7194  inf0  7324  trcl  7412  r1rankidb  7478  snwf  7483  unwf  7484  uniwf  7493  rankval3b  7500  rankr1a  7510  rankxplim3  7553  scott0  7558  card1  7603  pm54.43  7635  infxpenc2  7651  dfac8clem  7661  alephsuc2  7709  alephle  7717  cardaleph  7718  dfacacn  7769  dfac13  7770  dfac12lem2  7772  cdaval  7798  uncdadom  7799  cdaun  7800  cdacomen  7809  cdaassen  7810  cdadom1  7814  cdainf  7820  pwcda1  7822  ackbij1lem18  7865  cflem  7874  cflecard  7881  cfeq0  7884  cfslb  7894  cfsmolem  7898  cfcoflem  7900  cfidm  7903  isfin4-3  7943  fin23lem22  7955  fin23lem12  7959  fin23lem16  7963  fin23lem28  7968  fin23lem38  7977  fin23lem41  7980  fin1a2lem7  8034  fin1a2lem12  8039  fin1a2lem13  8040  hsmexlem8  8052  axcc2lem  8064  axcc3  8066  domtriomlem  8070  axdc3lem2  8079  axdc3lem4  8081  axdc4lem  8083  axcclem  8085  ac6num  8108  ttukeylem4  8141  ttukeylem7  8144  ttukey2g  8145  axdclem  8148  brdom3  8155  brdom5  8156  cardeq0  8176  unsnen  8177  konigthlem  8192  pwcfsdom  8207  canthp1lem1  8276  wunex2  8362  wuncval2  8371  eltsk2g  8375  intgru  8438  ingru  8439  grutsk  8446  axgroth6  8452  mulidpi  8512  nlt1pi  8532  indpi  8533  pinq  8553  mulidnq  8589  1idpr  8655  prlem934  8659  0idsr  8721  1idsr  8722  00sr  8723  negexsr  8726  recexsrlem  8727  sqgt0sr  8730  ax1rid  8785  axcnre  8788  ne0gt0  8927  peano2cn  8986  peano2re  8987  00id  8989  mul02lem2  8991  mul01  8993  subid  9069  subid1  9070  negid  9096  negeq0  9103  peano2rem  9115  lt0neg1  9282  le0neg1  9284  div2neg  9485  recgt0ii  9664  divgt0i2i  9674  ledivp1i  9684  ltdivp1i  9685  peano5nni  9751  peano2nn  9760  nnge1  9774  times2  9846  addltmul  9949  nn0p1nn  10005  peano2nn0  10006  elnnnn0  10009  nn0lele2xi  10018  peano2z  10062  peano2zm  10064  nn0lt10b  10080  suprzcl  10093  zeo  10099  uzindOLD  10108  uzwo  10283  uzwoOLD  10284  uzwo2  10285  infmssuzle  10302  infmssuzcl  10303  rpnnen1lem1  10344  rpnnen1lem3  10346  rpnnen1lem5  10348  rphalfcl  10380  ltpnf  10465  nltmnf  10470  pnfge  10471  nltpnft  10497  qsqueeze  10530  xlt0neg1  10548  xle0neg1  10550  xaddpnf1  10555  xaddmnf1  10557  xaddid1  10568  xsubge0  10583  xmul01  10589  xmulneg1  10591  xmulpnf1  10596  xmulid1  10601  supxrbnd  10649  supxrgtmnf  10650  supxrre1  10651  supxrre2  10652  elioopnf  10739  elicopnf  10741  iccshftri  10772  iccshftli  10774  iccdili  10776  icccntri  10778  fzprval  10846  fzofzp1  10918  fzostep1  10924  flge0nn0  10950  flge1nn  10951  btwnzge0  10955  modfrac  10986  om2uzsuci  11013  axdc4uzlem  11046  ser1const  11104  exp0  11110  exp1  11111  expn1  11115  expubnd  11164  sqval  11165  sqeq0  11170  resqcl  11173  zsqcl  11176  binom21  11221  expnbnd  11232  nn0opthlem2  11286  facnn2  11299  faclbnd4lem3  11310  faclbnd5  11313  bcnn  11326  bcn2  11333  hasheq0  11355  hashsng  11358  hashdif  11377  hashxplem  11387  hashf1lem2  11396  iswrd  11417  wrdval  11418  ccatval2  11434  ccatrid  11437  s111  11450  shftfib  11569  reim0  11605  imval2  11638  cjne0  11650  abssq  11793  max0add  11797  abs2dif  11818  rddif  11826  absrdbnd  11827  rexuz3  11834  rlimdm  12027  isershft  12139  isercolllem2  12141  isercoll  12143  fsum  12195  fsumadd  12213  bcxmas  12296  infcvgaux2i  12318  efi4p  12419  resin4p  12420  recos4p  12421  sinbnd  12462  cosbnd  12463  znnenlem  12492  rpnnen2lem8  12502  rpnnen2  12506  cnso  12527  dvdsmul2  12553  dvdslelem  12575  odd2np1lem  12588  divalglem0  12594  divalglem1  12595  divalglem4  12597  divalglem5  12598  divalglem8  12601  bits0  12621  bitsp1o  12626  bitsf1  12639  sadadd2lem2  12643  gcd1  12713  gcdmultiple  12731  isprm3  12769  phiprm  12847  pc0  12909  pcdvdstr  12930  vdwlem2  13031  vdwlem6  13035  vdwlem8  13037  hashbc0  13054  setsval  13174  setsres  13176  ressinbas  13206  ressress  13207  elrestr  13335  pwssnf1o  13399  xpsfrnel  13467  ismred2  13507  submre  13509  mreacs  13562  oppchomfval  13619  oppcbas  13623  brssc  13693  isssc  13699  yonedalem4c  14053  isprs  14066  lubid  14118  oduleval  14237  oduclatb  14250  gsumval2a  14461  mulg1  14576  mulgnegnn  14579  isghm  14685  cntrnsg  14819  oppgplusfval  14823  efgrelexlemb  15061  frgp0  15071  frgpmhm  15076  vrgpf  15079  cygctb  15180  dprd0  15268  dprd2da  15279  mgpplusg  15331  opprmulfval  15409  subrgint  15569  lsp0  15768  sralem  15932  zcyg  16447  mulgrhm2  16463  zlmsca  16477  chrnzr  16486  ocvz  16580  cssincl  16590  css0  16591  css1  16592  0opn  16652  topopn  16654  basdif0  16693  tgval  16695  unitg  16707  tgdif0  16732  isopn2  16771  0cld  16777  ntropn  16788  ntrval2  16790  ntrdif  16791  clsdif  16792  cmclsopn  16801  cmntrcld  16802  clstop  16808  ntrtop  16809  cls0  16819  ntr0  16820  mretopd  16831  neips  16852  maxlp  16880  isperf2  16885  rest0  16902  iocpnfordt  16947  icomnfordt  16948  mnfnei  16953  1stckgen  17251  ptbasfi  17278  pthaus  17334  fbssfi  17534  isfil2  17553  ssfg  17569  filcon  17580  fbasrn  17581  filufint  17617  imaelfm  17648  fmfnfmlem4  17654  fclsfnflim  17724  alexsubALTlem3  17745  alexsubALTlem4  17746  xmetres  17930  metres  17931  mopnex  18067  prdsms  18079  tngds  18166  nmoge0  18232  cnfldnm  18290  tgioo  18304  xrtgioo  18314  xrsmopn  18320  negcncf  18423  phtpy01  18485  pco0  18514  tchtopn  18659  tchnmfval  18661  caussi  18725  minveclem3b  18794  ovolfioo  18829  ovolficc  18830  ovolfsf  18833  ovolctb  18851  ovolctb2  18853  ovolfiniun  18862  ovoliun2  18867  ovolshftlem1  18870  ovolscalem1  18874  ovolicopnf  18885  iunmbl2  18916  uniioombllem2  18940  opnmblALT  18960  ismbf  18987  mbfinf  19022  0plef  19029  itg1climres  19071  itg2cnlem1  19118  iblitg  19125  ibl0  19143  itgcn  19199  cnlimc  19240  dvfre  19302  dvnfre  19303  dveflem  19328  dvef  19329  dvlipcn  19343  lhop2  19364  itgsubstlem  19397  evl1rhm  19414  ply1rem  19551  coefv0  19631  plyrecj  19662  vieta1lem2  19693  aannenlem1  19710  aaliou2b  19723  ulmval  19761  ulmpm  19764  ulmdvlem1  19779  mtest  19783  efcn  19821  sin2pim  19855  cos2pim  19856  sinmpi  19857  cosmpi  19858  sinppi  19859  cosppi  19860  efimpi  19861  sincosq1lem  19867  sincosq2sgn  19869  sincosq3sgn  19870  sincosq4sgn  19871  sinq12gt0  19877  sinq34lt0t  19879  sincosq1eq  19882  abssinper  19888  efif1o  19910  relogcn  19987  ellogdm  19988  efopn  20007  cxp0  20019  cxp1  20020  cxpsqr  20052  logsqr  20053  atandm3  20176  atanbnd  20224  atancn  20234  leibpi  20240  efrlim  20266  logdifbnd  20290  vmaprm  20357  ppip1le  20401  ppieq0  20416  prmorcht  20418  ppiublem1  20443  ppiub  20445  chpeq0  20449  chtub  20453  fsumvma  20454  pclogsum  20456  chpval2  20459  dchrresb  20500  dchrptlem1  20505  lgs0  20550  lgs2  20554  lgsdir2lem2  20565  lgsdir2lem4  20567  lgsdchrval  20588  lgsdchr  20589  lgseisenlem2  20591  dirith2  20679  selberg2lem  20701  qabvle  20776  qabvexp  20777  ostth  20790  ex-po  20824  gx1  20931  addinv  21021  vcoprne  21137  nvnd  21259  ipval2lem3  21280  ipval2  21282  ipval2lem6  21286  4ipval3  21287  ipidsq  21288  dipcj  21292  dip0r  21295  nmlnogt0  21377  blocni  21385  ipasslem2  21412  ipasslem8  21417  ipasslem9  21418  ajval  21442  ubthlem1  21451  hvaddid2  21604  hvsub0  21657  hi02  21678  hlimi  21769  isch2  21805  chlimi  21816  chsupunss  21925  shsupunss  21927  chlejb1i  22057  h1dei  22131  h1de2ci  22137  spanunsni  22160  pjoml2i  22166  pjorthi  22250  mayete3i  22309  mayete3iOLD  22310  hosubid1  22380  nmopge0  22493  nmfnge0  22509  adj1  22515  adjeq  22517  lnop0  22548  lnopmi  22582  nmophmi  22613  cnlnadjlem5  22653  cnlnadjeui  22659  unierri  22686  leoprf2  22709  leopnmid  22720  nmopleid  22721  hstles  22813  hst0  22815  strlem3a  22834  dmdbr2  22885  mdsl1i  22903  mdsl2i  22904  mdsl2bi  22905  cvmdi  22906  mdslmd1lem1  22907  mdslmd1lem2  22908  mdslmd1i  22911  mdslmd2i  22912  csmdsymi  22916  mdexchi  22917  superpos  22936  atomli  22964  atordi  22966  chirredlem1  22972  chirredlem2  22973  atcvat4i  22979  atabsi  22983  mdsymlem1  22985  mdsymlem5  22989  mdsymlem6  22990  sumdmdii  22997  dmdbr5ati  23004  dmdbr6ati  23005  mddmdin0i  23013  cdj3lem2  23017  infi  23031  ballotlemfcc  23054  infi1  23171  xppreima  23213  abfmpunirn  23218  abfmpel  23221  xrdifh  23275  xrmulc1cn  23305  xrge0neqmnf  23332  rge0scvg  23375  lmxrge0  23377  rnlogblem  23403  logb1  23407  esumcst  23438  hasheuni  23455  sgon  23487  dmvlsiga  23492  sigainb  23499  sigagenid  23513  measval  23531  ismeas  23532  probmeasb  23635  ptpcon  23766  cvmsss2  23807  cvmlift2lem12  23847  cvmlift2lem13  23848  cvmliftphtlem  23850  cvmliftpht  23851  umgra0  23879  iseupa  23883  relin01  24091  bcnm1  24098  fprb  24131  predreseq  24181  predep  24194  trpred0  24241  wfr3g  24257  wfrlem14  24271  wfrlem15  24272  frr3g  24282  noxpsgn  24321  elfix  24445  dffix2  24447  altopeq1  24499  brbtwn  24529  colinearalglem4  24539  axlowdimlem13  24584  axlowdimlem17  24588  brcolinear2  24683  bpoly2  24794  bpoly3  24795  bpoly4  24796  fsumcube  24797  ontgval  24872  onint1  24890  itg2addnclem  24933  itg2addnclem2  24934  itg2addnc  24935  condisd  24954  unfinsef  25080  prj1b  25090  prj3  25091  prl  25178  domncnt  25293  fprodp1i  25335  fprodp1fi  25339  fprodadd  25363  expm  25375  fprodneg  25389  fprodsub  25390  trooo  25405  rltrooo  25426  svli2  25495  topnem  25523  islimrs4  25593  bwt2  25603  claddrvr  25659  isnullcv  25663  rnegvex2  25672  negveudr  25680  clsmulrv  25694  divclrvd  25706  dualded  25794  dualcat2  25795  inttarcar  25912  prismorcsetlemc  25928  clscnc  26021  fnckle  26056  pgapspf2  26064  gtinf  26245  cldbnd  26255  ivthALT  26269  refref  26296  refssfne  26305  finptfin  26308  tailfb  26337  unirep  26360  sdclem2  26463  sstotbnd3  26511  totbndbnd  26524  heibor1lem  26544  heiborlem7  26552  bfplem1  26557  prnc  26703  fninfp  26765  fndifnfp  26767  fnnfpeq0  26769  ralxpmap  26772  mapfzcons1cl  26806  eldioph3b  26855  eldiophss  26865  0dioph  26869  vdioph  26870  eldioph4b  26905  eldioph4i  26906  rencldnfilem  26914  rmxy1  27018  rmxy0  27019  rmxm1  27030  rmym1  27031  monotoddzzfi  27038  nn0sqcl  27087  aomclem6  27167  pwslnmlem0  27204  pwslnmlem1  27205  isnumbasabl  27282  psgneldm2i  27439  seff  27549  lhe4.4ex1a  27557  fmuldfeqlem1  27723  stoweidlem22  27782  stoweidlem41  27801  stoweidlem59  27819  usisuslgra  28124  usgra0  28127  uvtx01vtx  28175  eelT0  28621  snssl  28678  bnj535  28995  bnj580  29018  bnj907  29070  bnj1253  29120  lub0N  29452  glb0N  29456  glbconN  29639  atpointN  30005  polsubN  30169  pol0N  30171  pol1N  30172  2polvalN  30176  2polssN  30177  3polN  30178  pcl0N  30184  2pmaplubN  30188  pnonsingN  30195  polsubclN  30214  cdleme31snd  30648  cdlemefs32sn1aw  30676  cdleme43fsv1snlem  30682  cdleme41sn3a  30695  cdleme32a  30703  cdleme40m  30729  cdleme40n  30730  cdleme42b  30740  istendo  31022  cdlemk40  31179  cdlemkid  31198  dihvalcqpre  31498
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