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  1902  eueq2  2940  sbcgf  3055  csbconstgf  3095  sbcnestg  3131  csbnestg  3132  csbnest1g  3134  mpteq1  4101  iinexg  4174  nnullss  4234  ord0eln0  4445  eusv2nf  4531  reusv2lem5  4538  eldifpw  4565  ordeleqon  4579  ordsson  4580  ssnlim  4673  xpss1  4794  xpiindi  4820  reldm0  4895  elrnmpt1s  4926  resdm  4992  resid  5005  eliniseg  5041  trinxp  5067  ssrnres  5115  coi2  5187  relrelss  5194  funcnvres  5287  funimaex  5296  fnresin1  5324  fnresin2  5325  fresin  5376  ssimaex  5546  dmfco  5555  fvmpt  5564  fvmptnf  5579  fvimacnvALT  5606  dff3  5635  fsn  5658  fsn2  5660  elabrex  5727  f1elima  5749  fliftel1  5771  f1owe  5812  2ndconst  6170  curry1  6172  tposfun  6212  tpostpos2  6217  sorpssuni  6248  sorpssint  6249  riotasv  6348  tfrlem10  6399  tfrlem12  6401  tfr3  6411  seqomlem1  6458  seqomlem2  6459  seqomlem4  6461  abianfplem  6466  ondif2  6497  oa0  6511  om0  6512  oa1suc  6526  om1  6536  oe1  6538  oe1m  6539  omass  6574  oeoalem  6590  oeoelem  6592  nnmsucr  6619  nnm1  6642  nnm2  6643  ecelqsg  6710  xpider  6726  qsel  6734  map0e  6801  fvdiagfn  6808  ixpsnf1o  6852  map1  6935  xp1en  6944  sbthlem7  6973  domunsn  7007  xpmapenlem  7024  infensuc  7035  diffi  7085  dif1enOLD  7086  dif1en  7087  unblem1  7105  unblem2  7106  unblem3  7107  unblem4  7108  isfinite2  7111  infn0  7115  unfilem1  7117  unfilem2  7118  unfir  7121  fofinf1o  7133  fidomdm  7134  cnvfi  7136  pwfilem  7146  mptfi  7151  finsschain  7158  marypha2  7188  inf0  7318  trcl  7406  r1rankidb  7472  snwf  7477  unwf  7478  uniwf  7487  rankval3b  7494  rankr1a  7504  rankxplim3  7547  scott0  7552  card1  7597  pm54.43  7629  infxpenc2  7645  dfac8clem  7655  alephsuc2  7703  alephle  7711  cardaleph  7712  dfacacn  7763  dfac13  7764  dfac12lem2  7766  cdaval  7792  uncdadom  7793  cdaun  7794  cdacomen  7803  cdaassen  7804  cdadom1  7808  cdainf  7814  pwcda1  7816  ackbij1lem18  7859  cflem  7868  cflecard  7875  cfeq0  7878  cfslb  7888  cfsmolem  7892  cfcoflem  7894  cfidm  7897  isfin4-3  7937  fin23lem22  7949  fin23lem12  7953  fin23lem16  7957  fin23lem28  7962  fin23lem38  7971  fin23lem41  7974  fin1a2lem7  8028  fin1a2lem12  8033  fin1a2lem13  8034  hsmexlem8  8046  axcc2lem  8058  axcc3  8060  domtriomlem  8064  axdc3lem2  8073  axdc3lem4  8075  axdc4lem  8077  axcclem  8079  ac6num  8102  ttukeylem4  8135  ttukeylem7  8138  ttukey2g  8139  axdclem  8142  brdom3  8149  brdom5  8150  cardeq0  8170  unsnen  8171  konigthlem  8186  pwcfsdom  8201  canthp1lem1  8270  wunex2  8356  wuncval2  8365  eltsk2g  8369  intgru  8432  ingru  8433  grutsk  8440  axgroth6  8446  mulidpi  8506  nlt1pi  8526  indpi  8527  pinq  8547  mulidnq  8583  1idpr  8649  prlem934  8653  0idsr  8715  1idsr  8716  00sr  8717  negexsr  8720  recexsrlem  8721  sqgt0sr  8724  ax1rid  8779  axcnre  8782  ne0gt0  8921  peano2cn  8980  peano2re  8981  00id  8983  mul02lem2  8985  mul01  8987  subid  9063  subid1  9064  negid  9090  negeq0  9097  peano2rem  9109  lt0neg1  9276  le0neg1  9278  div2neg  9479  recgt0ii  9658  divgt0i2i  9668  ledivp1i  9678  ltdivp1i  9679  peano5nni  9745  peano2nn  9754  nnge1  9768  times2  9840  addltmul  9943  nn0p1nn  9999  peano2nn0  10000  elnnnn0  10003  nn0lele2xi  10012  peano2z  10056  peano2zm  10058  nn0lt10b  10074  suprzcl  10087  zeo  10093  uzindOLD  10102  uzwo  10277  uzwoOLD  10278  uzwo2  10279  infmssuzle  10296  infmssuzcl  10297  rpnnen1lem1  10338  rpnnen1lem3  10340  rpnnen1lem5  10342  rphalfcl  10374  ltpnf  10459  nltmnf  10464  pnfge  10465  nltpnft  10491  qsqueeze  10524  xlt0neg1  10542  xle0neg1  10544  xaddpnf1  10549  xaddmnf1  10551  xaddid1  10562  xsubge0  10577  xmul01  10583  xmulneg1  10585  xmulpnf1  10590  xmulid1  10595  supxrbnd  10643  supxrgtmnf  10644  supxrre1  10645  supxrre2  10646  elioopnf  10733  elicopnf  10735  iccshftri  10766  iccshftli  10768  iccdili  10770  icccntri  10772  fzprval  10840  fzofzp1  10912  fzostep1  10918  flge0nn0  10944  flge1nn  10945  btwnzge0  10949  modfrac  10980  om2uzsuci  11007  axdc4uzlem  11040  ser1const  11098  exp0  11104  exp1  11105  expn1  11109  expubnd  11158  sqval  11159  sqeq0  11164  resqcl  11167  zsqcl  11170  binom21  11215  expnbnd  11226  nn0opthlem2  11280  facnn2  11293  faclbnd4lem3  11304  faclbnd5  11307  bcnn  11320  bcn2  11327  hasheq0  11349  hashsng  11352  hashdif  11371  hashxplem  11381  hashf1lem2  11390  iswrd  11411  wrdval  11412  ccatval2  11428  ccatrid  11431  s111  11444  shftfib  11563  reim0  11599  imval2  11632  cjne0  11644  abssq  11787  max0add  11791  abs2dif  11812  rddif  11820  absrdbnd  11821  rexuz3  11828  rlimdm  12021  isershft  12133  isercolllem2  12135  isercoll  12137  fsum  12189  fsumadd  12207  bcxmas  12290  infcvgaux2i  12312  efi4p  12413  resin4p  12414  recos4p  12415  sinbnd  12456  cosbnd  12457  znnenlem  12486  rpnnen2lem8  12496  rpnnen2  12500  cnso  12521  dvdsmul2  12547  dvdslelem  12569  odd2np1lem  12582  divalglem0  12588  divalglem1  12589  divalglem4  12591  divalglem5  12592  divalglem8  12595  bits0  12615  bitsp1o  12620  bitsf1  12633  sadadd2lem2  12637  gcd1  12707  gcdmultiple  12725  isprm3  12763  phiprm  12841  pc0  12903  pcdvdstr  12924  vdwlem2  13025  vdwlem6  13029  vdwlem8  13031  hashbc0  13048  setsval  13168  setsres  13170  ressinbas  13200  ressress  13201  elrestr  13329  pwssnf1o  13393  xpsfrnel  13461  ismred2  13501  submre  13503  mreacs  13556  oppchomfval  13613  oppcbas  13617  brssc  13687  isssc  13693  yonedalem4c  14047  isprs  14060  lubid  14112  oduleval  14231  oduclatb  14244  gsumval2a  14455  mulg1  14570  mulgnegnn  14573  isghm  14679  cntrnsg  14813  oppgplusfval  14817  efgrelexlemb  15055  frgp0  15065  frgpmhm  15070  vrgpf  15073  cygctb  15174  dprd0  15262  dprd2da  15273  mgpplusg  15325  opprmulfval  15403  subrgint  15563  lsp0  15762  sralem  15926  zcyg  16441  mulgrhm2  16457  zlmsca  16471  chrnzr  16480  ocvz  16574  cssincl  16584  css0  16585  css1  16586  0opn  16646  topopn  16648  basdif0  16687  tgval  16689  unitg  16701  tgdif0  16726  isopn2  16765  0cld  16771  ntropn  16782  ntrval2  16784  ntrdif  16785  clsdif  16786  cmclsopn  16795  cmntrcld  16796  clstop  16802  ntrtop  16803  cls0  16813  ntr0  16814  mretopd  16825  neips  16846  maxlp  16874  isperf2  16879  rest0  16896  iocpnfordt  16941  icomnfordt  16942  mnfnei  16947  1stckgen  17245  ptbasfi  17272  pthaus  17328  fbssfi  17528  isfil2  17547  ssfg  17563  filcon  17574  fbasrn  17575  filufint  17611  imaelfm  17642  fmfnfmlem4  17648  fclsfnflim  17718  alexsubALTlem3  17739  alexsubALTlem4  17740  xmetres  17924  metres  17925  mopnex  18061  prdsms  18073  tngds  18160  nmoge0  18226  cnfldnm  18284  tgioo  18298  xrtgioo  18308  xrsmopn  18314  negcncf  18417  phtpy01  18479  pco0  18508  tchtopn  18653  tchnmfval  18655  caussi  18719  minveclem3b  18788  ovolfioo  18823  ovolficc  18824  ovolfsf  18827  ovolctb  18845  ovolctb2  18847  ovolfiniun  18856  ovoliun2  18861  ovolshftlem1  18864  ovolscalem1  18868  ovolicopnf  18879  iunmbl2  18910  uniioombllem2  18934  opnmblALT  18954  ismbf  18981  mbfinf  19016  0plef  19023  itg1climres  19065  itg2cnlem1  19112  iblitg  19119  ibl0  19137  itgcn  19193  cnlimc  19234  dvfre  19296  dvnfre  19297  dveflem  19322  dvef  19323  dvlipcn  19337  lhop2  19358  itgsubstlem  19391  evl1rhm  19408  ply1rem  19545  coefv0  19625  plyrecj  19656  vieta1lem2  19687  aannenlem1  19704  aaliou2b  19717  ulmval  19755  ulmpm  19758  ulmdvlem1  19773  mtest  19777  efcn  19815  sin2pim  19849  cos2pim  19850  sinmpi  19851  cosmpi  19852  sinppi  19853  cosppi  19854  efimpi  19855  sincosq1lem  19861  sincosq2sgn  19863  sincosq3sgn  19864  sincosq4sgn  19865  sinq12gt0  19871  sinq34lt0t  19873  sincosq1eq  19876  abssinper  19882  efif1o  19904  relogcn  19981  ellogdm  19982  efopn  20001  cxp0  20013  cxp1  20014  cxpsqr  20046  logsqr  20047  atandm3  20170  atanbnd  20218  atancn  20228  leibpi  20234  efrlim  20260  logdifbnd  20284  vmaprm  20351  ppip1le  20395  ppieq0  20410  prmorcht  20412  ppiublem1  20437  ppiub  20439  chpeq0  20443  chtub  20447  fsumvma  20448  pclogsum  20450  chpval2  20453  dchrresb  20494  dchrptlem1  20499  lgs0  20544  lgs2  20548  lgsdir2lem2  20559  lgsdir2lem4  20561  lgsdchrval  20582  lgsdchr  20583  lgseisenlem2  20585  dirith2  20673  selberg2lem  20695  qabvle  20770  qabvexp  20771  ostth  20784  ex-po  20799  gx1  20923  addinv  21013  vcoprne  21129  nvnd  21251  ipval2lem3  21272  ipval2  21274  ipval2lem6  21278  4ipval3  21279  ipidsq  21280  dipcj  21284  dip0r  21287  nmlnogt0  21369  blocni  21377  ipasslem2  21404  ipasslem8  21409  ipasslem9  21410  ajval  21434  ubthlem1  21443  hvaddid2  21598  hvsub0  21651  hi02  21672  hlimi  21763  isch2  21799  chlimi  21810  chsupunss  21919  shsupunss  21921  chlejb1i  22051  h1dei  22125  h1de2ci  22131  spanunsni  22154  pjoml2i  22160  pjorthi  22244  mayete3i  22303  mayete3iOLD  22304  hosubid1  22374  nmopge0  22487  nmfnge0  22503  adj1  22509  adjeq  22511  lnop0  22542  lnopmi  22576  nmophmi  22607  cnlnadjlem5  22647  cnlnadjeui  22653  unierri  22680  leoprf2  22703  leopnmid  22714  nmopleid  22715  hstles  22807  hst0  22809  strlem3a  22828  dmdbr2  22879  mdsl1i  22897  mdsl2i  22898  mdsl2bi  22899  cvmdi  22900  mdslmd1lem1  22901  mdslmd1lem2  22902  mdslmd1i  22905  mdslmd2i  22906  csmdsymi  22910  mdexchi  22911  superpos  22930  atomli  22958  atordi  22960  chirredlem1  22966  chirredlem2  22967  atcvat4i  22973  atabsi  22977  mdsymlem1  22979  mdsymlem5  22983  mdsymlem6  22984  sumdmdii  22991  dmdbr5ati  22998  dmdbr6ati  22999  mddmdin0i  23007  cdj3lem2  23011  infi  23025  ballotlemfcc  23048  ptpcon  23171  cvmsss2  23212  cvmlift2lem12  23252  cvmlift2lem13  23253  cvmliftphtlem  23255  cvmliftpht  23256  umgra0  23284  iseupa  23288  relin01  23495  bcnm1  23502  fprb  23533  predreseq  23583  predep  23596  trpred0  23643  wfr3g  23659  wfrlem14  23673  wfrlem15  23674  frr3g  23684  noxpsgn  23722  elfix  23854  dffix2  23856  altopeq1  23907  brbtwn  23937  colinearalglem4  23947  axlowdimlem13  23992  axlowdimlem17  23996  brcolinear2  24091  bpoly2  24202  bpoly3  24203  bpoly4  24204  fsumcube  24205  ontgval  24280  onint1  24298  condisd  24353  unfinsef  24479  prj1b  24489  prj3  24490  cnveq3  24527  repfuntw  24571  prl  24578  domncnt  24693  fprodp1i  24735  fprodp1fi  24739  fprodadd  24763  expm  24775  fprodneg  24789  fprodsub  24790  trooo  24805  rltrooo  24826  svli2  24895  topnem  24923  islimrs4  24993  bwt2  25003  claddrvr  25059  isnullcv  25063  rnegvex2  25072  negveudr  25080  clsmulrv  25094  divclrvd  25106  dualded  25194  dualcat2  25195  inttarcar  25312  prismorcsetlemc  25328  clscnc  25421  fnckle  25456  pgapspf2  25464  gtinf  25645  cldbnd  25655  ivthALT  25669  refref  25696  refssfne  25705  finptfin  25708  tailfb  25737  unirep  25760  sdclem2  25863  sstotbnd3  25911  totbndbnd  25924  heibor1lem  25944  heiborlem7  25952  bfplem1  25957  prnc  26103  fninfp  26165  fndifnfp  26167  fnnfpeq0  26169  ralxpmap  26172  mapfzcons1cl  26206  eldioph3b  26255  eldiophss  26265  0dioph  26269  vdioph  26270  eldioph4b  26305  eldioph4i  26306  rencldnfilem  26314  rmxy1  26418  rmxy0  26419  rmxm1  26430  rmym1  26431  monotoddzzfi  26438  nn0sqcl  26487  aomclem6  26567  pwslnmlem0  26604  pwslnmlem1  26605  isnumbasabl  26682  psgneldm2i  26839  seff  26949  lhe4.4ex1a  26957  fmuldfeqlem1  27123  stoweidlem22  27182  stoweidlem41  27201  stoweidlem59  27219  eelT0  27830  snssl  27885  bnj535  28201  bnj580  28224  bnj907  28276  bnj1253  28326  lub0N  28658  glb0N  28662  glbconN  28845  atpointN  29211  polsubN  29375  pol0N  29377  pol1N  29378  2polvalN  29382  2polssN  29383  3polN  29384  pcl0N  29390  2pmaplubN  29394  pnonsingN  29401  polsubclN  29420  cdleme31snd  29854  cdlemefs32sn1aw  29882  cdleme43fsv1snlem  29888  cdleme41sn3a  29901  cdleme32a  29909  cdleme40m  29935  cdleme40n  29936  cdleme42b  29946  istendo  30228  cdlemk40  30385  cdlemkid  30404  dihvalcqpre  30704
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