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  1270  equs4  1972  eueq2  3025  sbcgf  3140  csbconstgf  3180  sbcnestg  3216  csbnestg  3217  csbnest1g  3219  mpteq1  4202  iinexg  4273  nnullss  4338  ord0eln0  4549  eusv2nf  4635  reusv2lem5  4642  eldifpw  4669  ordeleqon  4683  ordsson  4684  ssnlim  4777  xpss1  4898  xpiindi  4924  reldm0  4999  elrnmpt1s  5030  resdm  5096  resid  5109  eliniseg  5145  trinxp  5171  ssrnres  5219  cnveq0  5233  coi2  5292  relrelss  5299  funcnvres  5426  funimaex  5435  fnresin1  5463  fnresin2  5464  fresin  5516  dffv3  5628  ssimaex  5691  dmfco  5700  fvmpt  5709  fvmptnf  5724  fvimacnvALT  5751  dff3  5784  fsn  5807  fsn2  5809  elabrex  5885  f1elima  5909  fliftel1  5932  f1owe  5973  2ndconst  6336  curry1  6338  tposfun  6392  tpostpos2  6397  sorpssuni  6428  sorpssint  6429  riotasv  6494  tfrlem10  6545  tfrlem12  6547  tfr3  6557  seqomlem1  6604  seqomlem2  6605  seqomlem4  6607  abianfplem  6612  ondif2  6643  oa0  6657  om0  6658  oa1suc  6672  om1  6682  oe1  6684  oe1m  6685  omass  6720  oeoalem  6736  oeoelem  6738  nnmsucr  6765  nnm1  6788  nnm2  6789  ecelqsg  6856  xpider  6872  qsel  6880  map0e  6948  fvdiagfn  6955  ixpsnf1o  6999  map1  7082  xp1en  7091  sbthlem7  7120  domunsn  7154  xpmapenlem  7171  infensuc  7182  infi  7229  finresfin  7231  diffi  7236  dif1enOLD  7237  dif1en  7238  unblem1  7256  unblem2  7257  unblem3  7258  unblem4  7259  isfinite2  7262  infn0  7266  unfilem1  7268  unfilem2  7269  unfir  7272  fofinf1o  7284  fidomdm  7285  cnvfi  7287  pwfilem  7297  mptfi  7302  finsschain  7309  marypha2  7339  inf0  7469  trcl  7557  r1rankidb  7623  snwf  7628  unwf  7629  uniwf  7638  rankval3b  7645  rankr1a  7655  rankxplim3  7698  scott0  7703  card1  7748  pm54.43  7780  infxpenc2  7796  dfac8clem  7806  alephsuc2  7854  alephle  7862  cardaleph  7863  dfacacn  7914  dfac13  7915  dfac12lem2  7917  cdaval  7943  uncdadom  7944  cdaun  7945  cdacomen  7954  cdaassen  7955  cdadom1  7959  cdainf  7965  pwcda1  7967  ackbij1lem18  8010  cflem  8019  cflecard  8026  cfeq0  8029  cfslb  8039  cfsmolem  8043  cfcoflem  8045  cfidm  8048  isfin4-3  8088  fin23lem22  8100  fin23lem12  8104  fin23lem16  8108  fin23lem28  8113  fin23lem38  8122  fin23lem41  8125  fin1a2lem7  8179  fin1a2lem12  8184  fin1a2lem13  8185  hsmexlem8  8197  axcc2lem  8209  axcc3  8211  domtriomlem  8215  axdc3lem2  8224  axdc3lem4  8226  axdc4lem  8228  axcclem  8230  ac6num  8253  ttukeylem4  8286  ttukeylem7  8289  ttukey2g  8290  axdclem  8293  brdom3  8300  brdom5  8301  cardeq0  8321  unsnen  8322  konigthlem  8337  pwcfsdom  8352  canthp1lem1  8421  wunex2  8507  wuncval2  8516  eltsk2g  8520  intgru  8583  ingru  8584  grutsk  8591  axgroth6  8597  mulidpi  8657  nlt1pi  8677  indpi  8678  pinq  8698  mulidnq  8734  1idpr  8800  prlem934  8804  0idsr  8866  1idsr  8867  00sr  8868  negexsr  8871  recexsrlem  8872  sqgt0sr  8875  ax1rid  8930  axcnre  8933  ne0gt0  9072  peano2cn  9131  peano2re  9132  00id  9134  mul02lem2  9136  mul01  9138  subid  9214  subid1  9215  negid  9241  negeq0  9248  peano2rem  9260  lt0neg1  9427  le0neg1  9429  div2neg  9630  recgt0ii  9809  divgt0i2i  9819  ledivp1i  9829  ltdivp1i  9830  peano5nni  9896  peano2nn  9905  nnge1  9919  times2  9993  addltmul  10096  nn0p1nn  10152  peano2nn0  10153  elnnnn0  10156  nn0lele2xi  10165  peano2z  10211  peano2zm  10213  nn0lt10b  10229  suprzcl  10242  zeo  10248  uzindOLD  10257  uzwo  10432  uzwoOLD  10433  uzwo2  10434  infmssuzle  10451  infmssuzcl  10452  rpnnen1lem1  10493  rpnnen1lem3  10495  rpnnen1lem5  10497  rphalfcl  10529  ltpnf  10614  nltmnf  10619  pnfge  10620  nltpnft  10647  qsqueeze  10680  xlt0neg1  10698  xle0neg1  10700  xaddpnf1  10705  xaddmnf1  10707  xaddid1  10718  xsubge0  10733  xmul01  10739  xmulneg1  10741  xmulpnf1  10746  xmulid1  10751  supxrbnd  10800  supxrgtmnf  10801  supxrre1  10802  supxrre2  10803  elioopnf  10890  elicopnf  10892  iccshftri  10923  iccshftli  10925  iccdili  10927  icccntri  10929  fzprval  10997  fzofzp1  11076  fzostep1  11084  injresinj  11087  flge0nn0  11112  flge1nn  11113  btwnzge0  11117  modfrac  11148  om2uzsuci  11175  axdc4uzlem  11208  ser1const  11266  exp0  11273  exp1  11274  expn1  11278  expubnd  11327  sqval  11328  sqeq0  11333  resqcl  11336  zsqcl  11339  binom21  11384  expnbnd  11395  nn0opthlem2  11449  facnn2  11462  faclbnd4lem3  11473  faclbnd5  11476  bcnn  11490  bcn2  11497  bcn2p1  11503  hasheq0  11531  hashsng  11534  hashdif  11565  hash2pr  11574  hash2prde  11575  hashxplem  11583  hashf1lem2  11592  iswrd  11616  wrdval  11617  ccatval2  11633  ccatrid  11636  s111  11649  shftfib  11774  reim0  11810  imval2  11843  cjne0  11855  abssq  11998  max0add  12002  abs2dif  12023  rddif  12031  absrdbnd  12032  rexuz3  12039  rlimdm  12232  isershft  12344  isercolllem2  12346  isercoll  12348  fsum  12401  fsumadd  12419  bcxmas  12502  infcvgaux2i  12524  efi4p  12625  resin4p  12626  recos4p  12627  sinbnd  12668  cosbnd  12669  znnenlem  12698  rpnnen2lem8  12708  rpnnen2  12712  cnso  12733  dvdsmul2  12759  dvdslelem  12781  odd2np1lem  12794  divalglem0  12800  divalglem1  12801  divalglem4  12803  divalglem5  12804  divalglem8  12807  bits0  12827  bitsp1o  12832  bitsf1  12845  sadadd2lem2  12849  gcd1  12919  gcdmultiple  12937  isprm3  12975  phiprm  13053  pc0  13115  pcdvdstr  13136  vdwlem2  13237  vdwlem6  13241  vdwlem8  13243  hashbc0  13260  setsval  13380  setsres  13382  ressinbas  13412  ressress  13413  elrestr  13543  pwssnf1o  13607  xpsfrnel  13675  ismred2  13715  submre  13717  mreacs  13770  oppchomfval  13827  oppcbas  13831  brssc  13901  isssc  13907  yonedalem4c  14261  isprs  14274  lubid  14326  oduleval  14445  oduclatb  14458  gsumval2a  14669  mulg1  14784  mulgnegnn  14787  isghm  14893  cntrnsg  15027  oppgplusfval  15031  efgrelexlemb  15269  frgp0  15279  frgpmhm  15284  vrgpf  15287  cygctb  15388  dprd0  15476  dprd2da  15487  mgpplusg  15539  opprmulfval  15617  subrgint  15777  lsp0  15976  sralem  16140  zcyg  16662  mulgrhm2  16678  zlmsca  16692  chrnzr  16701  ocvz  16795  cssincl  16805  css0  16806  css1  16807  0opn  16867  topopn  16869  basdif0  16908  tgval  16910  unitg  16922  tgdif0  16947  isopn2  16986  0cld  16992  ntropn  17003  ntrval2  17005  ntrdif  17006  clsdif  17007  cmclsopn  17016  cmntrcld  17017  clstop  17023  ntrtop  17024  cls0  17034  ntr0  17035  mretopd  17046  neips  17067  maxlp  17095  isperf2  17100  rest0  17117  iocpnfordt  17162  icomnfordt  17163  mnfnei  17168  1stckgen  17466  ptbasfi  17493  pthaus  17549  fbssfi  17745  isfil2  17764  ssfg  17780  filcon  17791  fbasrn  17792  filufint  17828  imaelfm  17859  fmfnfmlem4  17865  fclsfnflim  17935  alexsubALTlem3  17956  alexsubALTlem4  17957  xmetres  18141  metres  18142  mopnex  18278  prdsms  18290  tngds  18377  nmoge0  18443  cnfldnm  18501  tgioo  18515  xrtgioo  18525  xrsmopn  18531  negcncf  18636  phtpy01  18698  pco0  18727  tchtopn  18872  tchnmfval  18874  caussi  18938  minveclem3b  19007  ovolfioo  19042  ovolficc  19043  ovolfsf  19046  ovolctb  19064  ovolctb2  19066  ovolfiniun  19075  ovoliun2  19080  ovolshftlem1  19083  ovolscalem1  19087  ovolicopnf  19098  iunmbl2  19129  uniioombllem2  19153  opnmblALT  19173  ismbf  19200  mbfinf  19235  0plef  19242  itg1climres  19284  itg2cnlem1  19331  iblitg  19338  ibl0  19356  itgcn  19412  cnlimc  19453  dvfre  19515  dvnfre  19516  dveflem  19541  dvef  19542  dvlipcn  19556  lhop2  19577  itgsubstlem  19610  evl1rhm  19627  ply1rem  19764  coefv0  19844  plyrecj  19875  vieta1lem2  19906  aannenlem1  19923  aaliou2b  19936  ulmval  19974  ulmpm  19977  ulmdvlem1  19994  mtest  19998  efcn  20037  sin2pim  20071  cos2pim  20072  sinmpi  20073  cosmpi  20074  sinppi  20075  cosppi  20076  efimpi  20077  sincosq1lem  20083  sincosq2sgn  20085  sincosq3sgn  20086  sincosq4sgn  20087  sinq12gt0  20093  sinq34lt0t  20095  sincosq1eq  20098  abssinper  20104  efif1o  20126  relogcn  20207  ellogdm  20208  efopn  20227  cxp0  20239  cxp1  20240  cxpsqr  20272  logsqr  20273  atandm3  20396  atanbnd  20444  atancn  20454  leibpi  20460  efrlim  20486  logdifbnd  20510  vmaprm  20578  ppip1le  20622  ppieq0  20637  prmorcht  20639  ppiublem1  20664  ppiub  20666  chpeq0  20670  chtub  20674  fsumvma  20675  pclogsum  20677  chpval2  20680  dchrresb  20721  dchrptlem1  20726  lgs0  20771  lgs2  20775  lgsdir2lem2  20786  lgsdir2lem4  20788  lgsdchrval  20809  lgsdchr  20810  lgseisenlem2  20812  dirith2  20900  selberg2lem  20922  qabvle  20997  qabvexp  20998  ostth  21011  uhgra0  21022  umgra0  21038  umisuhgra  21040  usisuslgra  21065  usgra0  21068  usgraedg4  21083  usgrafisbase  21098  ex-po  21133  gx1  21240  addinv  21330  vcoprne  21448  nvnd  21570  ipval2lem3  21591  ipval2  21593  ipval2lem6  21597  4ipval3  21598  ipidsq  21599  dipcj  21603  dip0r  21606  nmlnogt0  21688  blocni  21696  ipasslem2  21723  ipasslem8  21728  ipasslem9  21729  ajval  21753  ubthlem1  21762  hvaddid2  21915  hvsub0  21968  hi02  21989  hlimi  22080  isch2  22116  chlimi  22127  chsupunss  22236  shsupunss  22238  chlejb1i  22368  h1dei  22442  h1de2ci  22448  spanunsni  22471  pjoml2i  22477  pjorthi  22561  mayete3i  22620  mayete3iOLD  22621  hosubid1  22691  nmopge0  22804  nmfnge0  22820  adj1  22826  adjeq  22828  lnop0  22859  lnopmi  22893  nmophmi  22924  cnlnadjlem5  22964  cnlnadjeui  22970  unierri  22997  leoprf2  23020  leopnmid  23031  nmopleid  23032  hstles  23124  hst0  23126  strlem3a  23145  dmdbr2  23196  mdsl1i  23214  mdsl2i  23215  mdsl2bi  23216  cvmdi  23217  mdslmd1lem1  23218  mdslmd1lem2  23219  mdslmd1i  23222  mdslmd2i  23223  csmdsymi  23227  mdexchi  23228  superpos  23247  atomli  23275  atordi  23277  chirredlem1  23283  chirredlem2  23284  atcvat4i  23290  atabsi  23294  mdsymlem1  23296  mdsymlem5  23300  mdsymlem6  23301  sumdmdii  23308  dmdbr5ati  23315  dmdbr6ati  23316  mddmdin0i  23324  cdj3lem2  23328  inimasn  23434  xppreima  23461  abfmpunirn  23466  abfmpel  23469  xrdifh  23544  xrge0neqmnf  23603  neiptopnei  23644  xrmulc1cn  23671  rge0scvg  23690  lmxrge0  23692  ustfilxp  23717  ustuqtop1  23744  ustuqtop2  23745  ustuqtop3  23746  ustuqtop4  23747  utopsnneiplem  23750  ucnima  23775  blval2  23807  zrhre  23851  rnlogblem  23864  logb1  23868  esumcst  23920  esumfzf  23924  esumfsupre  23926  hasheuni  23940  sgon  23972  dmvlsiga  23977  sigainb  23984  sigagenid  23999  measval  24017  ismeas  24018  probmeasb  24136  rrvsum  24160  ballotlemfcc  24199  lgamgulmlem2  24262  ptpcon  24367  cvmsss2  24408  cvmlift2lem12  24448  cvmlift2lem13  24449  cvmliftphtlem  24451  cvmliftpht  24452  iseupa  24468  relin01  24678  bcnm1  24685  fprod  24751  risefac0  24815  fallfac0  24816  risefac1  24819  fallfac1  24820  fprb  24870  predreseq  24920  predep  24933  trpred0  24980  wfr3g  24996  wfrlem14  25010  wfrlem15  25011  frr3g  25021  noxpsgn  25060  elfix  25184  dffix2  25186  funpartfv  25225  altopeq1  25239  brbtwn  25269  colinearalglem4  25279  axlowdimlem13  25324  axlowdimlem17  25328  brcolinear2  25423  bpoly2  25534  bpoly3  25535  bpoly4  25536  fsumcube  25537  ontgval  25612  onint1  25630  itg2addnclem  25675  itg2addnclem2  25676  itg2addnc  25677  itg2gt0cn  25678  itgaddnclem2  25682  gtinf  25741  cldbnd  25751  ivthALT  25765  refref  25792  refssfne  25801  finptfin  25804  tailfb  25833  unirep  25856  sdclem2  25959  sstotbnd3  26006  totbndbnd  26019  heibor1lem  26039  heiborlem7  26047  bfplem1  26052  prnc  26198  fninfp  26260  fndifnfp  26262  fnnfpeq0  26264  ralxpmap  26267  mapfzcons1cl  26301  eldioph3b  26350  eldiophss  26360  0dioph  26364  vdioph  26365  eldioph4b  26400  eldioph4i  26401  rencldnfilem  26409  rmxy1  26513  rmxy0  26514  rmxm1  26525  rmym1  26526  monotoddzzfi  26533  nn0sqcl  26582  aomclem6  26662  pwslnmlem0  26699  pwslnmlem1  26700  isnumbasabl  26777  psgneldm2i  26934  seff  27044  lhe4.4ex1a  27052  fmuldfeqlem1  27218  stoweidlem22  27277  stoweidlem41  27296  stoweidlem59  27314  rlimdmafv  27548  usgrasscusgra  27648  uvtx01vtx  27657  fargshiftlem  27759  usgrcyclnl2  27767  constr3trl  27785  constr3pth  27786  constr3cycl  27787  4cycl4dv  27793  frgrancvvdeqlemA  27872  eelT0  28312  snssl  28369  bnj535  28686  bnj580  28709  bnj907  28761  bnj1253  28811  equs4NEW7  28956  lub0N  29450  glb0N  29454  glbconN  29637  atpointN  30003  polsubN  30167  pol0N  30169  pol1N  30170  2polvalN  30174  2polssN  30175  3polN  30176  pcl0N  30182  2pmaplubN  30186  pnonsingN  30193  polsubclN  30212  cdleme31snd  30646  cdlemefs32sn1aw  30674  cdleme43fsv1snlem  30680  cdleme41sn3a  30693  cdleme32a  30701  cdleme40m  30727  cdleme40n  30728  cdleme42b  30738  istendo  31020  cdlemk40  31177  cdlemkid  31196  dihvalcqpre  31496
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