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  3068  sbcgf  3184  csbconstgf  3224  sbcnestg  3260  csbnestg  3261  csbnest1g  3263  mpteq1  4249  iinexg  4320  nnullss  4385  ord0eln0  4595  eusv2nf  4680  reusv2lem5  4687  eldifpw  4714  ordeleqon  4728  ordsson  4729  ssnlim  4822  xpss1  4943  xpiindi  4969  reldm0  5046  elrnmpt1s  5077  resdm  5143  resid  5156  eliniseg  5192  trinxp  5218  inimasn  5248  ssrnres  5268  cnveq0  5286  coi2  5345  relrelss  5352  funcnvres  5481  funimaex  5490  fnresin1  5518  fnresin2  5519  fresin  5571  dffv3  5683  ssimaex  5747  dmfco  5756  fvmpt  5765  fvmptnf  5781  fvimacnvALT  5808  dff3  5841  fsn  5865  fsn2  5867  elabrex  5944  f1elima  5968  fliftel1  5991  f1owe  6032  2ndconst  6395  curry1  6397  tposfun  6454  tpostpos2  6459  sorpssuni  6490  sorpssint  6491  riotasv  6556  tfrlem10  6607  tfrlem12  6609  tfr3  6619  seqomlem1  6666  seqomlem2  6667  seqomlem4  6669  abianfplem  6674  ondif2  6705  oa0  6719  om0  6720  oa1suc  6734  om1  6744  oe1  6746  oe1m  6747  omass  6782  oeoalem  6798  oeoelem  6800  nnmsucr  6827  nnm1  6850  nnm2  6851  ecelqsg  6918  xpider  6934  qsel  6942  map0e  7010  fvdiagfn  7017  ixpsnf1o  7061  map1  7144  xp1en  7153  sbthlem7  7182  domunsn  7216  xpmapenlem  7233  infensuc  7244  infi  7291  finresfin  7293  diffi  7298  dif1enOLD  7299  dif1en  7300  unblem1  7318  unblem2  7319  unblem3  7320  unblem4  7321  isfinite2  7324  infn0  7328  unfilem1  7330  unfilem2  7331  unfir  7334  fofinf1o  7346  cnvfi  7349  pwfilem  7359  mptfi  7364  finsschain  7371  marypha2  7402  inf0  7532  trcl  7620  r1rankidb  7686  snwf  7691  unwf  7692  uniwf  7701  rankval3b  7708  rankr1a  7718  rankxplim3  7761  scott0  7766  card1  7811  pm54.43  7843  infxpenc2  7859  dfac8clem  7869  alephsuc2  7917  alephle  7925  cardaleph  7926  dfacacn  7977  dfac13  7978  dfac12lem2  7980  cdaval  8006  uncdadom  8007  cdaun  8008  cdacomen  8017  cdaassen  8018  cdadom1  8022  cdainf  8028  pwcda1  8030  ackbij1lem18  8073  cflem  8082  cflecard  8089  cfeq0  8092  cfslb  8102  cfsmolem  8106  cfcoflem  8108  cfidm  8111  isfin4-3  8151  fin23lem12  8167  fin23lem16  8171  fin23lem28  8176  fin23lem38  8185  fin23lem41  8188  fin1a2lem7  8242  fin1a2lem12  8247  fin1a2lem13  8248  hsmexlem8  8260  axcc2lem  8272  axcc3  8274  domtriomlem  8278  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  ac6num  8315  ttukeylem4  8348  ttukeylem7  8351  ttukey2g  8352  axdclem  8355  brdom3  8362  brdom5  8363  cardeq0  8383  unsnen  8384  konigthlem  8399  pwcfsdom  8414  canthp1lem1  8483  wunex2  8569  wuncval2  8578  eltsk2g  8582  intgru  8645  ingru  8646  grutsk  8653  axgroth6  8659  mulidpi  8719  nlt1pi  8739  indpi  8740  pinq  8760  mulidnq  8796  1idpr  8862  prlem934  8866  0idsr  8928  1idsr  8929  00sr  8930  negexsr  8933  recexsrlem  8934  sqgt0sr  8937  ax1rid  8992  axcnre  8995  ne0gt0  9134  peano2cn  9194  peano2re  9195  00id  9197  mul02lem2  9199  mul01  9201  subid  9277  subid1  9278  negid  9304  negeq0  9311  peano2rem  9323  lt0neg1  9490  le0neg1  9492  div2neg  9693  recgt0ii  9872  divgt0i2i  9882  ledivp1i  9892  ltdivp1i  9893  peano5nni  9959  peano2nn  9968  nnge1  9982  times2  10056  addltmul  10159  nn0p1nn  10215  peano2nn0  10216  elnnnn0  10219  nn0lele2xi  10228  peano2z  10274  peano2zm  10276  nn0lt10b  10292  suprzcl  10305  zeo  10311  uzindOLD  10320  uzwo  10495  uzwoOLD  10496  uzwo2  10497  infmssuzle  10514  infmssuzcl  10515  rpnnen1lem1  10556  rpnnen1lem3  10558  rpnnen1lem5  10560  rphalfcl  10592  ltpnf  10677  nltmnf  10682  pnfge  10683  nltpnft  10710  qsqueeze  10743  xlt0neg1  10761  xle0neg1  10763  xaddpnf1  10768  xaddmnf1  10770  xaddid1  10781  xsubge0  10796  xmul01  10802  xmulneg1  10804  xmulpnf1  10809  xmulid1  10814  supxrbnd  10863  supxrgtmnf  10864  supxrre1  10865  supxrre2  10866  elioopnf  10954  elicopnf  10956  iccshftri  10987  iccshftli  10989  iccdili  10991  icccntri  10993  fzprval  11062  fzofzp1  11144  fzostep1  11152  injresinj  11155  flge0nn0  11180  flge1nn  11181  btwnzge0  11185  modfrac  11216  om2uzsuci  11243  axdc4uzlem  11276  ser1const  11334  exp0  11341  exp1  11342  expn1  11346  expubnd  11395  sqval  11396  sqeq0  11401  resqcl  11404  zsqcl  11407  binom21  11452  expnbnd  11463  nn0opthlem2  11517  facnn2  11530  faclbnd4lem3  11541  faclbnd5  11544  bcnn  11558  bcn2  11565  bcn2p1  11571  hasheq0  11599  hashsng  11602  hashdif  11633  hash2pr  11642  hash2prde  11643  hashxplem  11651  hashf1lem2  11660  iswrd  11684  wrdval  11685  ccatval2  11701  ccatrid  11704  s111  11717  shftfib  11842  reim0  11878  imval2  11911  cjne0  11923  abssq  12066  max0add  12070  abs2dif  12091  rddif  12099  absrdbnd  12100  rexuz3  12107  rlimdm  12300  isershft  12412  isercolllem2  12414  isercoll  12416  fsum  12469  fsumadd  12487  bcxmas  12570  infcvgaux2i  12592  efi4p  12693  resin4p  12694  recos4p  12695  sinbnd  12736  cosbnd  12737  znnenlem  12766  rpnnen2lem8  12776  rpnnen2  12780  cnso  12801  dvdsmul2  12827  dvdslelem  12849  odd2np1lem  12862  divalglem0  12868  divalglem1  12869  divalglem4  12871  divalglem5  12872  divalglem8  12875  bits0  12895  bitsp1o  12900  bitsf1  12913  sadadd2lem2  12917  gcd1  12987  gcdmultiple  13005  isprm3  13043  phiprm  13121  pc0  13183  pcdvdstr  13204  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  hashbc0  13328  setsval  13448  setsres  13450  ressinbas  13480  ressress  13481  elrestr  13611  pwssnf1o  13675  xpsfrnel  13743  ismred2  13783  submre  13785  mreacs  13838  oppchomfval  13895  brssc  13969  isssc  13975  yonedalem4c  14329  isprs  14342  lubid  14394  oduleval  14513  oduclatb  14526  gsumval2a  14737  mulg1  14852  mulgnegnn  14855  isghm  14961  cntrnsg  15095  oppgplusfval  15099  efgrelexlemb  15337  frgp0  15347  frgpmhm  15352  vrgpf  15355  cygctb  15456  dprd0  15544  dprd2da  15555  mgpplusg  15607  opprmulfval  15685  subrgint  15845  lsp0  16040  sralem  16204  zcyg  16727  mulgrhm2  16743  zlmsca  16757  chrnzr  16766  ocvz  16860  cssincl  16870  css0  16871  css1  16872  0opn  16932  topopn  16934  basdif0  16973  tgval  16975  unitg  16987  tgdif0  17012  isopn2  17051  0cld  17057  ntropn  17068  ntrval2  17070  ntrdif  17071  clsdif  17072  cmclsopn  17081  cmntrcld  17082  clstop  17088  ntrtop  17089  cls0  17099  ntr0  17100  mretopd  17111  neips  17132  neiptopnei  17151  maxlp  17165  isperf2  17170  rest0  17187  iocpnfordt  17233  icomnfordt  17234  mnfnei  17239  1stckgen  17539  ptbasfi  17566  pthaus  17623  imasnopn  17675  imasncld  17676  imasncls  17677  fbssfi  17822  isfil2  17841  ssfg  17857  filcon  17868  fbasrn  17869  filufint  17905  imaelfm  17936  fmfnfmlem4  17942  fclsfnflim  18012  alexsubALTlem3  18033  alexsubALTlem4  18034  ustfilxp  18195  ustuqtop1  18224  ustuqtop2  18225  ustuqtop3  18226  ustuqtop4  18227  utopsnneiplem  18230  utopsnnei  18232  utop2nei  18233  cfiluweak  18278  neipcfilu  18279  xmetres  18347  metres  18348  mopnex  18502  prdsms  18514  blval2  18558  metucnOLD  18571  metucn  18572  tngds  18642  nmoge0  18708  cnfldnm  18766  tgioo  18780  xrtgioo  18790  xrsmopn  18796  negcncf  18901  phtpy01  18963  pco0  18992  tchtopn  19137  tchnmfval  19139  caussi  19203  minveclem3b  19282  ovolfioo  19317  ovolficc  19318  ovolfsf  19321  ovolctb  19339  ovolctb2  19341  ovolfiniun  19350  ovoliun2  19355  ovolshftlem1  19358  ovolscalem1  19362  ovolicopnf  19373  iunmbl2  19404  uniioombllem2  19428  opnmblALT  19448  ismbf  19475  mbfinf  19510  0plef  19517  itg1climres  19559  itg2cnlem1  19606  iblitg  19613  ibl0  19631  itgcn  19687  cnlimc  19728  dvfre  19790  dvnfre  19791  dveflem  19816  dvef  19817  dvlipcn  19831  lhop2  19852  itgsubstlem  19885  evl1rhm  19902  ply1rem  20039  coefv0  20119  plyrecj  20150  vieta1lem2  20181  aannenlem1  20198  aaliou2b  20211  ulmval  20249  ulmpm  20252  ulmdvlem1  20269  mtest  20273  efcn  20312  sin2pim  20346  cos2pim  20347  sinmpi  20348  cosmpi  20349  sinppi  20350  cosppi  20351  efimpi  20352  sincosq1lem  20358  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  sinq12gt0  20368  sinq34lt0t  20370  sincosq1eq  20373  abssinper  20379  efif1o  20401  relogcn  20482  ellogdm  20483  efopn  20502  cxp0  20514  cxp1  20515  cxpsqr  20547  logsqr  20548  atandm3  20671  atanbnd  20719  atancn  20729  leibpi  20735  efrlim  20761  logdifbnd  20785  vmaprm  20853  ppip1le  20897  ppieq0  20912  prmorcht  20914  ppiublem1  20939  ppiub  20941  chpeq0  20945  chtub  20949  fsumvma  20950  pclogsum  20952  chpval2  20955  dchrresb  20996  dchrptlem1  21001  lgs0  21046  lgs2  21050  lgsdir2lem2  21061  lgsdir2lem4  21063  lgsdchrval  21084  lgsdchr  21085  lgseisenlem2  21087  dirith2  21175  selberg2lem  21197  qabvle  21272  qabvexp  21273  ostth  21286  uhgra0  21297  umgra0  21313  umisuhgra  21315  usisuslgra  21340  usgra0  21343  usgraedg4  21359  usgrafisbase  21381  usgrasscusgra  21445  uvtx01vtx  21454  fargshiftlem  21574  usgrcyclnl2  21581  constr3trl  21599  constr3pth  21600  constr3cycl  21601  4cycl4dv  21607  iseupa  21640  ex-po  21696  gx1  21803  addinv  21893  vcoprne  22011  nvnd  22133  ipval2lem3  22154  ipval2  22156  ipval2lem6  22160  4ipval3  22161  ipidsq  22162  dipcj  22166  dip0r  22169  nmlnogt0  22251  blocni  22259  ipasslem2  22286  ipasslem8  22291  ipasslem9  22292  ajval  22316  ubthlem1  22325  hvaddid2  22478  hvsub0  22531  hi02  22552  hlimi  22643  isch2  22679  chlimi  22690  chsupunss  22799  shsupunss  22801  chlejb1i  22931  h1dei  23005  h1de2ci  23011  spanunsni  23034  pjoml2i  23040  pjorthi  23124  mayete3i  23183  mayete3iOLD  23184  hosubid1  23254  nmopge0  23367  nmfnge0  23383  adj1  23389  adjeq  23391  lnop0  23422  lnopmi  23456  nmophmi  23487  cnlnadjlem5  23527  cnlnadjeui  23533  unierri  23560  leoprf2  23583  leopnmid  23594  nmopleid  23595  hstles  23687  hst0  23689  strlem3a  23708  dmdbr2  23759  mdsl1i  23777  mdsl2i  23778  mdsl2bi  23779  cvmdi  23780  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd1i  23785  mdslmd2i  23786  csmdsymi  23790  mdexchi  23791  superpos  23810  atomli  23838  atordi  23840  chirredlem1  23846  chirredlem2  23847  atcvat4i  23853  atabsi  23857  mdsymlem1  23859  mdsymlem5  23863  mdsymlem6  23864  sumdmdii  23871  dmdbr5ati  23878  dmdbr6ati  23879  mddmdin0i  23887  cdj3lem2  23891  xppreima  24012  abfmpunirn  24017  abfmpel  24020  xlemnf  24070  xrdifh  24096  clatp0ex  24146  clatp1ex  24147  xrge0neqmnf  24165  metider  24242  rge0scvg  24288  lmxrge0  24290  qqh0  24321  qqh1  24322  zrhre  24338  rnlogblem  24352  logb1  24356  esumcst  24408  esumfzf  24412  esumfsupre  24414  hasheuni  24428  sgon  24460  dmvlsiga  24465  sigainb  24472  measval  24505  ismeas  24506  sxbrsigalem0  24574  rrvsum  24665  ballotlem2  24699  ballotlemfcc  24704  ballotlem4  24709  ptpcon  24873  cvmsss2  24914  cvmlift2lem12  24954  cvmlift2lem13  24955  cvmliftphtlem  24957  cvmliftpht  24958  relin01  25147  bcnm1  25154  fprod  25220  risefac0  25295  fallfac0  25296  risefac1  25299  fallfac1  25300  fprb  25343  predreseq  25393  predep  25406  trpred0  25453  wfr3g  25469  wfrlem14  25483  wfrlem15  25484  frr3g  25494  noxpsgn  25533  elfix  25657  dffix2  25659  funpartfv  25698  altopeq1  25712  brbtwn  25742  colinearalglem4  25752  axlowdimlem13  25797  axlowdimlem17  25801  brcolinear2  25896  bpoly2  26007  bpoly3  26008  bpoly4  26009  fsumcube  26010  ontgval  26085  onint1  26103  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  gtinf  26212  cldbnd  26219  ivthALT  26228  refref  26255  refssfne  26264  tailfb  26296  unirep  26304  sdclem2  26336  totbndbnd  26388  heibor1lem  26408  heiborlem7  26416  bfplem1  26421  prnc  26567  fninfp  26625  fndifnfp  26627  fnnfpeq0  26629  ralxpmap  26632  mapfzcons1cl  26664  eldioph3b  26713  eldiophss  26723  0dioph  26727  vdioph  26728  eldioph4b  26762  eldioph4i  26763  rencldnfilem  26771  rmxy1  26875  rmxy0  26876  rmxm1  26887  rmym1  26888  monotoddzzfi  26895  nn0sqcl  26944  aomclem6  27024  pwslnmlem0  27061  pwslnmlem1  27062  isnumbasabl  27139  psgneldm2i  27296  seff  27406  lhe4.4ex1a  27414  fmuldfeqlem1  27579  fmuldfeq  27580  infrglb  27589  climneg  27603  stoweidlem18  27634  stoweidlem19  27635  stoweidlem22  27638  stoweidlem34  27650  stoweidlem40  27656  stoweidlem41  27657  stoweidlem55  27671  stoweidlem59  27675  rlimdmafv  27908  cnm1cn  27968  euhash1  27998  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  el2wlkonotlem  28059  usg2wlkonot  28080  usg2wotspth  28081  frgrancvvdeqlemA  28140  eelT0  28596  snssl  28651  bnj535  28967  bnj580  28990  bnj907  29042  bnj1253  29092  equs4NEW7  29237  lub0N  29672  glb0N  29676  glbconN  29859  atpointN  30225  polsubN  30389  pol0N  30391  pol1N  30392  2polvalN  30396  2polssN  30397  3polN  30398  pcl0N  30404  2pmaplubN  30408  pnonsingN  30415  polsubclN  30434  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32a  30923  cdleme40m  30949  cdleme40n  30950  cdleme42b  30960  istendo  31242  cdlemk40  31399  cdlemkid  31418  dihvalcqpre  31718
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