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  1899  eueq2  2939  sbcgf  3054  csbconstgf  3094  sbcnestg  3130  csbnestg  3131  csbnest1g  3133  mpteq1  4100  iinexg  4171  nnullss  4235  ord0eln0  4446  eusv2nf  4532  reusv2lem5  4539  eldifpw  4566  ordeleqon  4580  ordsson  4581  ssnlim  4674  xpss1  4795  xpiindi  4821  reldm0  4896  elrnmpt1s  4927  resdm  4993  resid  5006  eliniseg  5042  trinxp  5068  ssrnres  5116  cnveq0  5130  coi2  5189  relrelss  5196  funcnvres  5321  funimaex  5330  fnresin1  5358  fnresin2  5359  fresin  5410  dffv3  5521  ssimaex  5584  dmfco  5593  fvmpt  5602  fvmptnf  5617  fvimacnvALT  5644  dff3  5673  fsn  5696  fsn2  5698  elabrex  5765  f1elima  5787  fliftel1  5809  f1owe  5850  2ndconst  6208  curry1  6210  tposfun  6250  tpostpos2  6255  sorpssuni  6286  sorpssint  6287  riotasv  6352  tfrlem10  6403  tfrlem12  6405  tfr3  6415  seqomlem1  6462  seqomlem2  6463  seqomlem4  6465  abianfplem  6470  ondif2  6501  oa0  6515  om0  6516  oa1suc  6530  om1  6540  oe1  6542  oe1m  6543  omass  6578  oeoalem  6594  oeoelem  6596  nnmsucr  6623  nnm1  6646  nnm2  6647  ecelqsg  6714  xpider  6730  qsel  6738  map0e  6805  fvdiagfn  6812  ixpsnf1o  6856  map1  6939  xp1en  6948  sbthlem7  6977  domunsn  7011  xpmapenlem  7028  infensuc  7039  diffi  7089  dif1enOLD  7090  dif1en  7091  unblem1  7109  unblem2  7110  unblem3  7111  unblem4  7112  isfinite2  7115  infn0  7119  unfilem1  7121  unfilem2  7122  unfir  7125  fofinf1o  7137  fidomdm  7138  cnvfi  7140  pwfilem  7150  mptfi  7155  finsschain  7162  marypha2  7192  inf0  7322  trcl  7410  r1rankidb  7476  snwf  7481  unwf  7482  uniwf  7491  rankval3b  7498  rankr1a  7508  rankxplim3  7551  scott0  7556  card1  7601  pm54.43  7633  infxpenc2  7649  dfac8clem  7659  alephsuc2  7707  alephle  7715  cardaleph  7716  dfacacn  7767  dfac13  7768  dfac12lem2  7770  cdaval  7796  uncdadom  7797  cdaun  7798  cdacomen  7807  cdaassen  7808  cdadom1  7812  cdainf  7818  pwcda1  7820  ackbij1lem18  7863  cflem  7872  cflecard  7879  cfeq0  7882  cfslb  7892  cfsmolem  7896  cfcoflem  7898  cfidm  7901  isfin4-3  7941  fin23lem22  7953  fin23lem12  7957  fin23lem16  7961  fin23lem28  7966  fin23lem38  7975  fin23lem41  7978  fin1a2lem7  8032  fin1a2lem12  8037  fin1a2lem13  8038  hsmexlem8  8050  axcc2lem  8062  axcc3  8064  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  ac6num  8106  ttukeylem4  8139  ttukeylem7  8142  ttukey2g  8143  axdclem  8146  brdom3  8153  brdom5  8154  cardeq0  8174  unsnen  8175  konigthlem  8190  pwcfsdom  8205  canthp1lem1  8274  wunex2  8360  wuncval2  8369  eltsk2g  8373  intgru  8436  ingru  8437  grutsk  8444  axgroth6  8450  mulidpi  8510  nlt1pi  8530  indpi  8531  pinq  8551  mulidnq  8587  1idpr  8653  prlem934  8657  0idsr  8719  1idsr  8720  00sr  8721  negexsr  8724  recexsrlem  8725  sqgt0sr  8728  ax1rid  8783  axcnre  8786  ne0gt0  8925  peano2cn  8984  peano2re  8985  00id  8987  mul02lem2  8989  mul01  8991  subid  9067  subid1  9068  negid  9094  negeq0  9101  peano2rem  9113  lt0neg1  9280  le0neg1  9282  div2neg  9483  recgt0ii  9662  divgt0i2i  9672  ledivp1i  9682  ltdivp1i  9683  peano5nni  9749  peano2nn  9758  nnge1  9772  times2  9844  addltmul  9947  nn0p1nn  10003  peano2nn0  10004  elnnnn0  10007  nn0lele2xi  10016  peano2z  10060  peano2zm  10062  nn0lt10b  10078  suprzcl  10091  zeo  10097  uzindOLD  10106  uzwo  10281  uzwoOLD  10282  uzwo2  10283  infmssuzle  10300  infmssuzcl  10301  rpnnen1lem1  10342  rpnnen1lem3  10344  rpnnen1lem5  10346  rphalfcl  10378  ltpnf  10463  nltmnf  10468  pnfge  10469  nltpnft  10495  qsqueeze  10528  xlt0neg1  10546  xle0neg1  10548  xaddpnf1  10553  xaddmnf1  10555  xaddid1  10566  xsubge0  10581  xmul01  10587  xmulneg1  10589  xmulpnf1  10594  xmulid1  10599  supxrbnd  10647  supxrgtmnf  10648  supxrre1  10649  supxrre2  10650  elioopnf  10737  elicopnf  10739  iccshftri  10770  iccshftli  10772  iccdili  10774  icccntri  10776  fzprval  10844  fzofzp1  10916  fzostep1  10922  flge0nn0  10948  flge1nn  10949  btwnzge0  10953  modfrac  10984  om2uzsuci  11011  axdc4uzlem  11044  ser1const  11102  exp0  11108  exp1  11109  expn1  11113  expubnd  11162  sqval  11163  sqeq0  11168  resqcl  11171  zsqcl  11174  binom21  11219  expnbnd  11230  nn0opthlem2  11284  facnn2  11297  faclbnd4lem3  11308  faclbnd5  11311  bcnn  11324  bcn2  11331  hasheq0  11353  hashsng  11356  hashdif  11375  hashxplem  11385  hashf1lem2  11394  iswrd  11415  wrdval  11416  ccatval2  11432  ccatrid  11435  s111  11448  shftfib  11567  reim0  11603  imval2  11636  cjne0  11648  abssq  11791  max0add  11795  abs2dif  11816  rddif  11824  absrdbnd  11825  rexuz3  11832  rlimdm  12025  isershft  12137  isercolllem2  12139  isercoll  12141  fsum  12193  fsumadd  12211  bcxmas  12294  infcvgaux2i  12316  efi4p  12417  resin4p  12418  recos4p  12419  sinbnd  12460  cosbnd  12461  znnenlem  12490  rpnnen2lem8  12500  rpnnen2  12504  cnso  12525  dvdsmul2  12551  dvdslelem  12573  odd2np1lem  12586  divalglem0  12592  divalglem1  12593  divalglem4  12595  divalglem5  12596  divalglem8  12599  bits0  12619  bitsp1o  12624  bitsf1  12637  sadadd2lem2  12641  gcd1  12711  gcdmultiple  12729  isprm3  12767  phiprm  12845  pc0  12907  pcdvdstr  12928  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  hashbc0  13052  setsval  13172  setsres  13174  ressinbas  13204  ressress  13205  elrestr  13333  pwssnf1o  13397  xpsfrnel  13465  ismred2  13505  submre  13507  mreacs  13560  oppchomfval  13617  oppcbas  13621  brssc  13691  isssc  13697  yonedalem4c  14051  isprs  14064  lubid  14116  oduleval  14235  oduclatb  14248  gsumval2a  14459  mulg1  14574  mulgnegnn  14577  isghm  14683  cntrnsg  14817  oppgplusfval  14821  efgrelexlemb  15059  frgp0  15069  frgpmhm  15074  vrgpf  15077  cygctb  15178  dprd0  15266  dprd2da  15277  mgpplusg  15329  opprmulfval  15407  subrgint  15567  lsp0  15766  sralem  15930  zcyg  16445  mulgrhm2  16461  zlmsca  16475  chrnzr  16484  ocvz  16578  cssincl  16588  css0  16589  css1  16590  0opn  16650  topopn  16652  basdif0  16691  tgval  16693  unitg  16705  tgdif0  16730  isopn2  16769  0cld  16775  ntropn  16786  ntrval2  16788  ntrdif  16789  clsdif  16790  cmclsopn  16799  cmntrcld  16800  clstop  16806  ntrtop  16807  cls0  16817  ntr0  16818  mretopd  16829  neips  16850  maxlp  16878  isperf2  16883  rest0  16900  iocpnfordt  16945  icomnfordt  16946  mnfnei  16951  1stckgen  17249  ptbasfi  17276  pthaus  17332  fbssfi  17532  isfil2  17551  ssfg  17567  filcon  17578  fbasrn  17579  filufint  17615  imaelfm  17646  fmfnfmlem4  17652  fclsfnflim  17722  alexsubALTlem3  17743  alexsubALTlem4  17744  xmetres  17928  metres  17929  mopnex  18065  prdsms  18077  tngds  18164  nmoge0  18230  cnfldnm  18288  tgioo  18302  xrtgioo  18312  xrsmopn  18318  negcncf  18421  phtpy01  18483  pco0  18512  tchtopn  18657  tchnmfval  18659  caussi  18723  minveclem3b  18792  ovolfioo  18827  ovolficc  18828  ovolfsf  18831  ovolctb  18849  ovolctb2  18851  ovolfiniun  18860  ovoliun2  18865  ovolshftlem1  18868  ovolscalem1  18872  ovolicopnf  18883  iunmbl2  18914  uniioombllem2  18938  opnmblALT  18958  ismbf  18985  mbfinf  19020  0plef  19027  itg1climres  19069  itg2cnlem1  19116  iblitg  19123  ibl0  19141  itgcn  19197  cnlimc  19238  dvfre  19300  dvnfre  19301  dveflem  19326  dvef  19327  dvlipcn  19341  lhop2  19362  itgsubstlem  19395  evl1rhm  19412  ply1rem  19549  coefv0  19629  plyrecj  19660  vieta1lem2  19691  aannenlem1  19708  aaliou2b  19721  ulmval  19759  ulmpm  19762  ulmdvlem1  19777  mtest  19781  efcn  19819  sin2pim  19853  cos2pim  19854  sinmpi  19855  cosmpi  19856  sinppi  19857  cosppi  19858  efimpi  19859  sincosq1lem  19865  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  sinq12gt0  19875  sinq34lt0t  19877  sincosq1eq  19880  abssinper  19886  efif1o  19908  relogcn  19985  ellogdm  19986  efopn  20005  cxp0  20017  cxp1  20018  cxpsqr  20050  logsqr  20051  atandm3  20174  atanbnd  20222  atancn  20232  leibpi  20238  efrlim  20264  logdifbnd  20288  vmaprm  20355  ppip1le  20399  ppieq0  20414  prmorcht  20416  ppiublem1  20441  ppiub  20443  chpeq0  20447  chtub  20451  fsumvma  20452  pclogsum  20454  chpval2  20457  dchrresb  20498  dchrptlem1  20503  lgs0  20548  lgs2  20552  lgsdir2lem2  20563  lgsdir2lem4  20565  lgsdchrval  20586  lgsdchr  20587  lgseisenlem2  20589  dirith2  20677  selberg2lem  20699  qabvle  20774  qabvexp  20775  ostth  20788  ex-po  20822  gx1  20929  addinv  21019  vcoprne  21135  nvnd  21257  ipval2lem3  21278  ipval2  21280  ipval2lem6  21284  4ipval3  21285  ipidsq  21286  dipcj  21290  dip0r  21293  nmlnogt0  21375  blocni  21383  ipasslem2  21410  ipasslem8  21415  ipasslem9  21416  ajval  21440  ubthlem1  21449  hvaddid2  21602  hvsub0  21655  hi02  21676  hlimi  21767  isch2  21803  chlimi  21814  chsupunss  21923  shsupunss  21925  chlejb1i  22055  h1dei  22129  h1de2ci  22135  spanunsni  22158  pjoml2i  22164  pjorthi  22248  mayete3i  22307  mayete3iOLD  22308  hosubid1  22378  nmopge0  22491  nmfnge0  22507  adj1  22513  adjeq  22515  lnop0  22546  lnopmi  22580  nmophmi  22611  cnlnadjlem5  22651  cnlnadjeui  22657  unierri  22684  leoprf2  22707  leopnmid  22718  nmopleid  22719  hstles  22811  hst0  22813  strlem3a  22832  dmdbr2  22883  mdsl1i  22901  mdsl2i  22902  mdsl2bi  22903  cvmdi  22904  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd1i  22909  mdslmd2i  22910  csmdsymi  22914  mdexchi  22915  superpos  22934  atomli  22962  atordi  22964  chirredlem1  22970  chirredlem2  22971  atcvat4i  22977  atabsi  22981  mdsymlem1  22983  mdsymlem5  22987  mdsymlem6  22988  sumdmdii  22995  dmdbr5ati  23002  dmdbr6ati  23003  mddmdin0i  23011  cdj3lem2  23015  infi  23029  ballotlemfcc  23052  infi1  23169  xppreima  23211  abfmpunirn  23216  abfmpel  23219  xrdifh  23273  xrmulc1cn  23303  xrge0neqmnf  23330  rge0scvg  23373  lmxrge0  23375  rnlogblem  23401  logb1  23405  esumcst  23436  hasheuni  23453  sgon  23485  dmvlsiga  23490  sigainb  23497  sigagenid  23511  measval  23529  ismeas  23530  probmeasb  23633  ptpcon  23764  cvmsss2  23805  cvmlift2lem12  23845  cvmlift2lem13  23846  cvmliftphtlem  23848  cvmliftpht  23849  umgra0  23877  iseupa  23881  relin01  24089  bcnm1  24096  fprb  24129  predreseq  24179  predep  24192  trpred0  24239  wfr3g  24255  wfrlem14  24269  wfrlem15  24270  frr3g  24280  noxpsgn  24319  elfix  24443  dffix2  24445  altopeq1  24497  brbtwn  24527  colinearalglem4  24537  axlowdimlem13  24582  axlowdimlem17  24586  brcolinear2  24681  bpoly2  24792  bpoly3  24793  bpoly4  24794  fsumcube  24795  ontgval  24870  onint1  24888  condisd  24943  unfinsef  25069  prj1b  25079  prj3  25080  prl  25167  domncnt  25282  fprodp1i  25324  fprodp1fi  25328  fprodadd  25352  expm  25364  fprodneg  25378  fprodsub  25379  trooo  25394  rltrooo  25415  svli2  25484  topnem  25512  islimrs4  25582  bwt2  25592  claddrvr  25648  isnullcv  25652  rnegvex2  25661  negveudr  25669  clsmulrv  25683  divclrvd  25695  dualded  25783  dualcat2  25784  inttarcar  25901  prismorcsetlemc  25917  clscnc  26010  fnckle  26045  pgapspf2  26053  gtinf  26234  cldbnd  26244  ivthALT  26258  refref  26285  refssfne  26294  finptfin  26297  tailfb  26326  unirep  26349  sdclem2  26452  sstotbnd3  26500  totbndbnd  26513  heibor1lem  26533  heiborlem7  26541  bfplem1  26546  prnc  26692  fninfp  26754  fndifnfp  26756  fnnfpeq0  26758  ralxpmap  26761  mapfzcons1cl  26795  eldioph3b  26844  eldiophss  26854  0dioph  26858  vdioph  26859  eldioph4b  26894  eldioph4i  26895  rencldnfilem  26903  rmxy1  27007  rmxy0  27008  rmxm1  27019  rmym1  27020  monotoddzzfi  27027  nn0sqcl  27076  aomclem6  27156  pwslnmlem0  27193  pwslnmlem1  27194  isnumbasabl  27271  psgneldm2i  27428  seff  27538  lhe4.4ex1a  27546  fmuldfeqlem1  27712  stoweidlem22  27771  stoweidlem41  27790  stoweidlem59  27808  usisuslgra  28113  usgra0  28116  uvtx01vtx  28164  eelT0  28550  snssl  28605  bnj535  28922  bnj580  28945  bnj907  28997  bnj1253  29047  lub0N  29379  glb0N  29383  glbconN  29566  atpointN  29932  polsubN  30096  pol0N  30098  pol1N  30099  2polvalN  30103  2polssN  30104  3polN  30105  pcl0N  30111  2pmaplubN  30115  pnonsingN  30122  polsubclN  30141  cdleme31snd  30575  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme41sn3a  30622  cdleme32a  30630  cdleme40m  30656  cdleme40n  30657  cdleme42b  30667  istendo  30949  cdlemk40  31106  cdlemkid  31125  dihvalcqpre  31425
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