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

Theorem mpan2 653
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 11 . 2  |-  ( ph  ->  ps )
3 mpan2.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpdan 650 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpanr12  667  mp3an23  1271  equs4OLD  1952  eueq2  3076  sbcgf  3192  csbconstgf  3232  sbcnestg  3268  csbnestg  3269  csbnest1g  3271  mpteq1  4257  iinexg  4328  nnullss  4393  ord0eln0  4603  eusv2nf  4688  reusv2lem5  4695  eldifpw  4722  ordeleqon  4736  ordsson  4737  ssnlim  4830  xpss1  4951  xpiindi  4977  reldm0  5054  elrnmpt1s  5085  resdm  5151  resid  5164  eliniseg  5200  trinxp  5226  inimasn  5256  ssrnres  5276  cnveq0  5294  coi2  5353  relrelss  5360  funcnvres  5489  funimaex  5498  fnresin1  5526  fnresin2  5527  fresin  5579  dffv3  5691  ssimaex  5755  dmfco  5764  fvmpt  5773  fvmptnf  5789  fvimacnvALT  5816  dff3  5849  fsn  5873  fsn2  5875  elabrex  5952  f1elima  5976  fliftel1  5999  f1owe  6040  2ndconst  6403  curry1  6405  tposfun  6462  tpostpos2  6467  sorpssuni  6498  sorpssint  6499  riotasv  6564  tfrlem10  6615  tfrlem12  6617  tfr3  6627  seqomlem1  6674  seqomlem2  6675  seqomlem4  6677  abianfplem  6682  ondif2  6713  oa0  6727  om0  6728  oa1suc  6742  om1  6752  oe1  6754  oe1m  6755  omass  6790  oeoalem  6806  oeoelem  6808  nnmsucr  6835  nnm1  6858  nnm2  6859  ecelqsg  6926  xpider  6942  qsel  6950  map0e  7018  fvdiagfn  7025  ixpsnf1o  7069  map1  7152  xp1en  7161  sbthlem7  7190  domunsn  7224  xpmapenlem  7241  infensuc  7252  infi  7299  finresfin  7301  diffi  7306  dif1enOLD  7307  dif1en  7308  unblem1  7326  unblem2  7327  unblem3  7328  unblem4  7329  isfinite2  7332  infn0  7336  unfilem1  7338  unfilem2  7339  unfir  7342  fofinf1o  7354  cnvfi  7357  pwfilem  7367  mptfi  7372  finsschain  7379  marypha2  7410  inf0  7540  trcl  7628  r1rankidb  7694  snwf  7699  unwf  7700  uniwf  7709  rankval3b  7716  rankr1a  7726  rankxplim3  7769  scott0  7774  card1  7819  pm54.43  7851  infxpenc2  7867  dfac8clem  7877  alephsuc2  7925  alephle  7933  cardaleph  7934  dfacacn  7985  dfac13  7986  dfac12lem2  7988  cdaval  8014  uncdadom  8015  cdaun  8016  cdacomen  8025  cdaassen  8026  cdadom1  8030  cdainf  8036  pwcda1  8038  ackbij1lem18  8081  cflem  8090  cflecard  8097  cfeq0  8100  cfslb  8110  cfsmolem  8114  cfcoflem  8116  cfidm  8119  isfin4-3  8159  fin23lem12  8175  fin23lem16  8179  fin23lem28  8184  fin23lem38  8193  fin23lem41  8196  fin1a2lem7  8250  fin1a2lem12  8255  fin1a2lem13  8256  hsmexlem8  8268  axcc2lem  8280  axcc3  8282  domtriomlem  8286  axdc3lem2  8295  axdc3lem4  8297  axdc4lem  8299  axcclem  8301  ac6num  8323  ttukeylem4  8356  ttukeylem7  8359  ttukey2g  8360  axdclem  8363  brdom3  8370  brdom5  8371  cardeq0  8391  unsnen  8392  konigthlem  8407  pwcfsdom  8422  canthp1lem1  8491  wunex2  8577  wuncval2  8586  eltsk2g  8590  intgru  8653  ingru  8654  grutsk  8661  axgroth6  8667  mulidpi  8727  nlt1pi  8747  indpi  8748  pinq  8768  mulidnq  8804  1idpr  8870  prlem934  8874  0idsr  8936  1idsr  8937  00sr  8938  negexsr  8941  recexsrlem  8942  sqgt0sr  8945  ax1rid  9000  axcnre  9003  ne0gt0  9142  peano2cn  9202  peano2re  9203  00id  9205  mul02lem2  9207  mul01  9209  subid  9285  subid1  9286  negid  9312  negeq0  9319  peano2rem  9331  lt0neg1  9498  le0neg1  9500  div2neg  9701  recgt0ii  9880  divgt0i2i  9890  ledivp1i  9900  ltdivp1i  9901  peano5nni  9967  peano2nn  9976  nnge1  9990  times2  10064  addltmul  10167  nn0p1nn  10223  peano2nn0  10224  elnnnn0  10227  nn0lele2xi  10236  peano2z  10282  peano2zm  10284  nn0lt10b  10300  suprzcl  10313  zeo  10319  uzindOLD  10328  uzwo  10503  uzwoOLD  10504  uzwo2  10505  infmssuzle  10522  infmssuzcl  10523  rpnnen1lem1  10564  rpnnen1lem3  10566  rpnnen1lem5  10568  rphalfcl  10600  ltpnf  10685  nltmnf  10690  pnfge  10691  nltpnft  10718  qsqueeze  10751  xlt0neg1  10769  xle0neg1  10771  xaddpnf1  10776  xaddmnf1  10778  xaddid1  10789  xsubge0  10804  xmul01  10810  xmulneg1  10812  xmulpnf1  10817  xmulid1  10822  supxrbnd  10871  supxrgtmnf  10872  supxrre1  10873  supxrre2  10874  elioopnf  10962  elicopnf  10964  iccshftri  10995  iccshftli  10997  iccdili  10999  icccntri  11001  fzprval  11070  fzofzp1  11152  fzostep1  11160  injresinj  11163  flge0nn0  11188  flge1nn  11189  btwnzge0  11193  modfrac  11224  om2uzsuci  11251  axdc4uzlem  11284  ser1const  11342  exp0  11349  exp1  11350  expn1  11354  expubnd  11403  sqval  11404  sqeq0  11409  resqcl  11412  zsqcl  11415  binom21  11460  expnbnd  11471  nn0opthlem2  11525  facnn2  11538  faclbnd4lem3  11549  faclbnd5  11552  bcnn  11566  bcn2  11573  bcn2p1  11579  hasheq0  11607  hashsng  11610  hashdif  11641  hash2pr  11650  hash2prde  11651  hashxplem  11659  hashf1lem2  11668  iswrd  11692  wrdval  11693  ccatval2  11709  ccatrid  11712  s111  11725  shftfib  11850  reim0  11886  imval2  11919  cjne0  11931  abssq  12074  max0add  12078  abs2dif  12099  rddif  12107  absrdbnd  12108  rexuz3  12115  rlimdm  12308  isershft  12420  isercolllem2  12422  isercoll  12424  fsum  12477  fsumadd  12495  bcxmas  12578  infcvgaux2i  12600  efi4p  12701  resin4p  12702  recos4p  12703  sinbnd  12744  cosbnd  12745  znnenlem  12774  rpnnen2lem8  12784  rpnnen2  12788  cnso  12809  dvdsmul2  12835  dvdslelem  12857  odd2np1lem  12870  divalglem0  12876  divalglem1  12877  divalglem4  12879  divalglem5  12880  divalglem8  12883  bits0  12903  bitsp1o  12908  bitsf1  12921  sadadd2lem2  12925  gcd1  12995  gcdmultiple  13013  isprm3  13051  phiprm  13129  pc0  13191  pcdvdstr  13212  vdwlem2  13313  vdwlem6  13317  vdwlem8  13319  hashbc0  13336  setsval  13456  setsres  13458  ressinbas  13488  ressress  13489  elrestr  13619  pwssnf1o  13683  xpsfrnel  13751  ismred2  13791  submre  13793  mreacs  13846  oppchomfval  13903  brssc  13977  isssc  13983  yonedalem4c  14337  isprs  14350  lubid  14402  oduleval  14521  oduclatb  14534  gsumval2a  14745  mulg1  14860  mulgnegnn  14863  isghm  14969  cntrnsg  15103  oppgplusfval  15107  efgrelexlemb  15345  frgp0  15355  frgpmhm  15360  vrgpf  15363  cygctb  15464  dprd0  15552  dprd2da  15563  mgpplusg  15615  opprmulfval  15693  subrgint  15853  lsp0  16048  sralem  16212  zcyg  16735  mulgrhm2  16751  zlmsca  16765  chrnzr  16774  ocvz  16868  cssincl  16878  css0  16879  css1  16880  0opn  16940  topopn  16942  basdif0  16981  tgval  16983  unitg  16995  tgdif0  17020  isopn2  17059  0cld  17065  ntropn  17076  ntrval2  17078  ntrdif  17079  clsdif  17080  cmclsopn  17089  cmntrcld  17090  clstop  17096  ntrtop  17097  cls0  17107  ntr0  17108  mretopd  17119  neips  17140  neiptopnei  17159  maxlp  17173  isperf2  17178  rest0  17195  iocpnfordt  17241  icomnfordt  17242  mnfnei  17247  1stckgen  17547  ptbasfi  17574  pthaus  17631  imasnopn  17683  imasncld  17684  imasncls  17685  fbssfi  17830  isfil2  17849  ssfg  17865  filcon  17876  fbasrn  17877  filufint  17913  imaelfm  17944  fmfnfmlem4  17950  fclsfnflim  18020  alexsubALTlem3  18041  alexsubALTlem4  18042  ustfilxp  18203  ustuqtop1  18232  ustuqtop2  18233  ustuqtop3  18234  ustuqtop4  18235  utopsnneiplem  18238  utopsnnei  18240  utop2nei  18241  cfiluweak  18286  neipcfilu  18287  xmetres  18355  metres  18356  mopnex  18510  prdsms  18522  blval2  18566  metucnOLD  18579  metucn  18580  tngds  18650  nmoge0  18716  cnfldnm  18774  tgioo  18788  xrtgioo  18798  xrsmopn  18804  negcncf  18909  phtpy01  18971  pco0  19000  tchtopn  19145  tchnmfval  19147  caussi  19211  minveclem3b  19290  ovolfioo  19325  ovolficc  19326  ovolfsf  19329  ovolctb  19347  ovolctb2  19349  ovolfiniun  19358  ovoliun2  19363  ovolshftlem1  19366  ovolscalem1  19370  ovolicopnf  19381  iunmbl2  19412  uniioombllem2  19436  opnmblALT  19456  ismbf  19483  mbfinf  19518  0plef  19525  itg1climres  19567  itg2cnlem1  19614  iblitg  19621  ibl0  19639  itgcn  19695  cnlimc  19736  dvfre  19798  dvnfre  19799  dveflem  19824  dvef  19825  dvlipcn  19839  lhop2  19860  itgsubstlem  19893  evl1rhm  19910  ply1rem  20047  coefv0  20127  plyrecj  20158  vieta1lem2  20189  aannenlem1  20206  aaliou2b  20219  ulmval  20257  ulmpm  20260  ulmdvlem1  20277  mtest  20281  efcn  20320  sin2pim  20354  cos2pim  20355  sinmpi  20356  cosmpi  20357  sinppi  20358  cosppi  20359  efimpi  20360  sincosq1lem  20366  sincosq2sgn  20368  sincosq3sgn  20369  sincosq4sgn  20370  sinq12gt0  20376  sinq34lt0t  20378  sincosq1eq  20381  abssinper  20387  efif1o  20409  relogcn  20490  ellogdm  20491  efopn  20510  cxp0  20522  cxp1  20523  cxpsqr  20555  logsqr  20556  atandm3  20679  atanbnd  20727  atancn  20737  leibpi  20743  efrlim  20769  logdifbnd  20793  vmaprm  20861  ppip1le  20905  ppieq0  20920  prmorcht  20922  ppiublem1  20947  ppiub  20949  chpeq0  20953  chtub  20957  fsumvma  20958  pclogsum  20960  chpval2  20963  dchrresb  21004  dchrptlem1  21009  lgs0  21054  lgs2  21058  lgsdir2lem2  21069  lgsdir2lem4  21071  lgsdchrval  21092  lgsdchr  21093  lgseisenlem2  21095  dirith2  21183  selberg2lem  21205  qabvle  21280  qabvexp  21281  ostth  21294  uhgra0  21305  umgra0  21321  umisuhgra  21323  usisuslgra  21348  usgra0  21351  usgraedg4  21367  usgrafisbase  21389  usgrasscusgra  21453  uvtx01vtx  21462  fargshiftlem  21582  usgrcyclnl2  21589  constr3trl  21607  constr3pth  21608  constr3cycl  21609  4cycl4dv  21615  iseupa  21648  ex-po  21704  gx1  21811  addinv  21901  vcoprne  22019  nvnd  22141  ipval2lem3  22162  ipval2  22164  ipval2lem6  22168  4ipval3  22169  ipidsq  22170  dipcj  22174  dip0r  22177  nmlnogt0  22259  blocni  22267  ipasslem2  22294  ipasslem8  22299  ipasslem9  22300  ajval  22324  ubthlem1  22333  hvaddid2  22486  hvsub0  22539  hi02  22560  hlimi  22651  isch2  22687  chlimi  22698  chsupunss  22807  shsupunss  22809  chlejb1i  22939  h1dei  23013  h1de2ci  23019  spanunsni  23042  pjoml2i  23048  pjorthi  23132  mayete3i  23191  mayete3iOLD  23192  hosubid1  23262  nmopge0  23375  nmfnge0  23391  adj1  23397  adjeq  23399  lnop0  23430  lnopmi  23464  nmophmi  23495  cnlnadjlem5  23535  cnlnadjeui  23541  unierri  23568  leoprf2  23591  leopnmid  23602  nmopleid  23603  hstles  23695  hst0  23697  strlem3a  23716  dmdbr2  23767  mdsl1i  23785  mdsl2i  23786  mdsl2bi  23787  cvmdi  23788  mdslmd1lem1  23789  mdslmd1lem2  23790  mdslmd1i  23793  mdslmd2i  23794  csmdsymi  23798  mdexchi  23799  superpos  23818  atomli  23846  atordi  23848  chirredlem1  23854  chirredlem2  23855  atcvat4i  23861  atabsi  23865  mdsymlem1  23867  mdsymlem5  23871  mdsymlem6  23872  sumdmdii  23879  dmdbr5ati  23886  dmdbr6ati  23887  mddmdin0i  23895  cdj3lem2  23899  xppreima  24020  abfmpunirn  24025  abfmpel  24028  xlemnf  24078  xrdifh  24104  clatp0ex  24154  clatp1ex  24155  xrge0neqmnf  24173  metider  24250  rge0scvg  24296  lmxrge0  24298  qqh0  24329  qqh1  24330  zrhre  24346  rnlogblem  24360  logb1  24364  esumcst  24416  esumfzf  24420  esumfsupre  24422  hasheuni  24436  sgon  24468  dmvlsiga  24473  sigainb  24480  measval  24513  ismeas  24514  sxbrsigalem0  24582  rrvsum  24673  ballotlem2  24707  ballotlemfcc  24712  ballotlem4  24717  ptpcon  24881  cvmsss2  24922  cvmlift2lem12  24962  cvmlift2lem13  24963  cvmliftphtlem  24965  cvmliftpht  24966  relin01  25155  bcnm1  25162  fprod  25228  risefac0  25303  fallfac0  25304  risefac1  25307  fallfac1  25308  fprb  25351  predreseq  25401  predep  25414  trpred0  25461  wfr3g  25477  wfrlem14  25491  wfrlem15  25492  frr3g  25502  noxpsgn  25541  elfix  25665  dffix2  25667  funpartfv  25706  altopeq1  25720  brbtwn  25750  colinearalglem4  25760  axlowdimlem13  25805  axlowdimlem17  25809  brcolinear2  25904  bpoly2  26015  bpoly3  26016  bpoly4  26017  fsumcube  26018  ontgval  26093  onint1  26111  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  itg2addnclem  26163  itg2addnclem2  26164  itg2addnclem3  26165  itg2addnc  26166  itg2gt0cn  26167  gtinf  26220  cldbnd  26227  ivthALT  26236  refref  26263  refssfne  26272  tailfb  26304  unirep  26312  sdclem2  26344  totbndbnd  26396  heibor1lem  26416  heiborlem7  26424  bfplem1  26429  prnc  26575  fninfp  26633  fndifnfp  26635  fnnfpeq0  26637  ralxpmap  26640  mapfzcons1cl  26672  eldioph3b  26721  eldiophss  26731  0dioph  26735  vdioph  26736  eldioph4b  26770  eldioph4i  26771  rencldnfilem  26779  rmxy1  26883  rmxy0  26884  rmxm1  26895  rmym1  26896  monotoddzzfi  26903  nn0sqcl  26952  aomclem6  27032  pwslnmlem0  27069  pwslnmlem1  27070  isnumbasabl  27147  psgneldm2i  27304  seff  27414  lhe4.4ex1a  27422  fmuldfeqlem1  27587  fmuldfeq  27588  infrglb  27597  climneg  27611  stoweidlem18  27642  stoweidlem19  27643  stoweidlem22  27646  stoweidlem34  27658  stoweidlem40  27664  stoweidlem41  27665  stoweidlem55  27679  stoweidlem59  27683  rlimdmafv  27916  cnm1cn  27976  euhash1  28006  swrdccat3b  28039  usgra2pthspth  28043  usgra2wlkspthlem2  28045  usgra2pthlem1  28048  el2wlkonotlem  28067  usg2wlkonot  28088  usg2wotspth  28089  frgrancvvdeqlemA  28148  eelT0  28605  snssl  28660  bnj535  28979  bnj580  29002  bnj907  29054  bnj1253  29104  equs4NEW7  29249  lub0N  29684  glb0N  29688  glbconN  29871  atpointN  30237  polsubN  30401  pol0N  30403  pol1N  30404  2polvalN  30408  2polssN  30409  3polN  30410  pcl0N  30416  2pmaplubN  30420  pnonsingN  30427  polsubclN  30446  cdlemefs32sn1aw  30908  cdleme43fsv1snlem  30914  cdleme41sn3a  30927  cdleme32a  30935  cdleme40m  30961  cdleme40n  30962  cdleme42b  30972  istendo  31254  cdlemk40  31411  cdlemkid  31430  dihvalcqpre  31730
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 178  df-an 361
  Copyright terms: Public domain W3C validator