MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan2 Structured version   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  1998  eueq2  3108  sbcgf  3224  csbconstgf  3264  sbcnestg  3300  csbnestg  3301  csbnest1g  3303  mpteq1  4289  iinexg  4360  nnullss  4425  ord0eln0  4635  eusv2nf  4721  reusv2lem5  4728  eldifpw  4755  ordeleqon  4769  ordsson  4770  ssnlim  4863  xpss1  4984  xpiindi  5010  reldm0  5087  elrnmpt1s  5118  resdm  5184  resid  5197  eliniseg  5233  trinxp  5259  inimasn  5289  ssrnres  5309  cnveq0  5327  coi2  5386  relrelss  5393  funcnvres  5522  funimaex  5531  fnresin1  5559  fnresin2  5560  fresin  5612  dffv3  5724  ssimaex  5788  dmfco  5797  fvmpt  5806  fvmptnf  5822  fvimacnvALT  5849  dff3  5882  fsn  5906  fsn2  5908  elabrex  5985  f1elima  6009  fliftel1  6032  f1owe  6073  2ndconst  6436  curry1  6438  tposfun  6495  tpostpos2  6500  sorpssuni  6531  sorpssint  6532  riotasv  6597  tfrlem10  6648  tfrlem12  6650  tfr3  6660  seqomlem1  6707  seqomlem2  6708  seqomlem4  6710  abianfplem  6715  ondif2  6746  oa0  6760  om0  6761  oa1suc  6775  om1  6785  oe1  6787  oe1m  6788  omass  6823  oeoalem  6839  oeoelem  6841  nnmsucr  6868  nnm1  6891  nnm2  6892  ecelqsg  6959  xpider  6975  qsel  6983  map0e  7051  fvdiagfn  7058  ixpsnf1o  7102  map1  7185  xp1en  7194  sbthlem7  7223  domunsn  7257  xpmapenlem  7274  infensuc  7285  infi  7332  finresfin  7334  diffi  7339  dif1enOLD  7340  dif1en  7341  unblem1  7359  unblem2  7360  unblem3  7361  unblem4  7362  isfinite2  7365  infn0  7369  unfilem1  7371  unfilem2  7372  unfir  7375  fofinf1o  7387  cnvfi  7390  pwfilem  7401  mptfi  7406  finsschain  7413  marypha2  7444  inf0  7576  trcl  7664  r1rankidb  7730  snwf  7735  unwf  7736  uniwf  7745  rankval3b  7752  rankr1a  7762  rankxplim3  7805  scott0  7810  card1  7855  pm54.43  7887  infxpenc2  7903  dfac8clem  7913  alephsuc2  7961  alephle  7969  cardaleph  7970  dfacacn  8021  dfac13  8022  dfac12lem2  8024  cdaval  8050  uncdadom  8051  cdaun  8052  cdacomen  8061  cdaassen  8062  cdadom1  8066  cdainf  8072  pwcda1  8074  ackbij1lem18  8117  cflem  8126  cflecard  8133  cfeq0  8136  cfslb  8146  cfsmolem  8150  cfcoflem  8152  cfidm  8155  isfin4-3  8195  fin23lem12  8211  fin23lem16  8215  fin23lem28  8220  fin23lem38  8229  fin23lem41  8232  fin1a2lem7  8286  fin1a2lem12  8291  fin1a2lem13  8292  hsmexlem8  8304  axcc2lem  8316  axcc3  8318  domtriomlem  8322  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  axcclem  8337  ac6num  8359  ttukeylem4  8392  ttukeylem7  8395  ttukey2g  8396  axdclem  8399  brdom3  8406  brdom5  8407  cardeq0  8427  unsnen  8428  konigthlem  8443  pwcfsdom  8458  canthp1lem1  8527  wunex2  8613  wuncval2  8622  eltsk2g  8626  intgru  8689  ingru  8690  grutsk  8697  axgroth6  8703  mulidpi  8763  nlt1pi  8783  indpi  8784  pinq  8804  mulidnq  8840  1idpr  8906  prlem934  8910  0idsr  8972  1idsr  8973  00sr  8974  negexsr  8977  recexsrlem  8978  sqgt0sr  8981  ax1rid  9036  axcnre  9039  ne0gt0  9178  peano2cn  9238  peano2re  9239  00id  9241  mul02lem2  9243  mul01  9245  subid  9321  subid1  9322  negid  9348  negeq0  9355  peano2rem  9367  lt0neg1  9534  le0neg1  9536  div2neg  9737  recgt0ii  9916  divgt0i2i  9926  ledivp1i  9936  ltdivp1i  9937  peano5nni  10003  peano2nn  10012  nnge1  10026  times2  10100  addltmul  10203  nn0p1nn  10259  peano2nn0  10260  elnnnn0  10263  nn0lele2xi  10272  peano2z  10318  peano2zm  10320  nn0lt10b  10336  suprzcl  10349  zeo  10355  uzindOLD  10364  uzwo  10539  uzwoOLD  10540  uzwo2  10541  infmssuzle  10558  infmssuzcl  10559  rpnnen1lem1  10600  rpnnen1lem3  10602  rpnnen1lem5  10604  rphalfcl  10636  ltpnf  10721  nltmnf  10726  pnfge  10727  nltpnft  10754  qsqueeze  10787  xlt0neg1  10805  xle0neg1  10807  xaddpnf1  10812  xaddmnf1  10814  xaddid1  10825  xsubge0  10840  xmul01  10846  xmulneg1  10848  xmulpnf1  10853  xmulid1  10858  supxrbnd  10907  supxrgtmnf  10908  supxrre1  10909  supxrre2  10910  elioopnf  10998  elicopnf  11000  iccshftri  11031  iccshftli  11033  iccdili  11035  icccntri  11037  fzprval  11106  fzofzp1  11189  fzostep1  11197  injresinj  11200  flge0nn0  11225  flge1nn  11226  btwnzge0  11230  modfrac  11261  om2uzsuci  11288  axdc4uzlem  11321  ser1const  11379  exp0  11386  exp1  11387  expn1  11391  expubnd  11440  sqval  11441  sqeq0  11446  resqcl  11449  zsqcl  11452  binom21  11497  expnbnd  11508  nn0opthlem2  11562  facnn2  11575  faclbnd4lem3  11586  faclbnd5  11589  bcnn  11603  bcn2  11610  bcn2p1  11616  hasheq0  11644  hashsng  11647  hashdif  11678  hash2pr  11687  hash2prde  11688  hashxplem  11696  hashf1lem2  11705  iswrd  11729  wrdval  11730  ccatval2  11746  ccatrid  11749  s111  11762  shftfib  11887  reim0  11923  imval2  11956  cjne0  11968  abssq  12111  max0add  12115  abs2dif  12136  rddif  12144  absrdbnd  12145  rexuz3  12152  rlimdm  12345  isershft  12457  isercolllem2  12459  isercoll  12461  fsum  12514  fsumadd  12532  bcxmas  12615  infcvgaux2i  12637  efi4p  12738  resin4p  12739  recos4p  12740  sinbnd  12781  cosbnd  12782  znnenlem  12811  rpnnen2lem8  12821  rpnnen2  12825  cnso  12846  dvdsmul2  12872  dvdslelem  12894  odd2np1lem  12907  divalglem0  12913  divalglem1  12914  divalglem4  12916  divalglem5  12917  divalglem8  12920  bits0  12940  bitsp1o  12945  bitsf1  12958  sadadd2lem2  12962  gcd1  13032  gcdmultiple  13050  isprm3  13088  phiprm  13166  pc0  13228  pcdvdstr  13249  vdwlem2  13350  vdwlem6  13354  vdwlem8  13356  hashbc0  13373  setsval  13493  setsres  13495  ressinbas  13525  ressress  13526  elrestr  13656  pwssnf1o  13720  xpsfrnel  13788  ismred2  13828  submre  13830  mreacs  13883  oppchomfval  13940  brssc  14014  isssc  14020  yonedalem4c  14374  isprs  14387  lubid  14439  oduleval  14558  oduclatb  14571  gsumval2a  14782  mulg1  14897  mulgnegnn  14900  isghm  15006  cntrnsg  15140  oppgplusfval  15144  efgrelexlemb  15382  frgp0  15392  frgpmhm  15397  vrgpf  15400  cygctb  15501  dprd0  15589  dprd2da  15600  mgpplusg  15652  opprmulfval  15730  subrgint  15890  lsp0  16085  sralem  16249  zcyg  16772  mulgrhm2  16788  zlmsca  16802  chrnzr  16811  ocvz  16905  cssincl  16915  css0  16916  css1  16917  0opn  16977  topopn  16979  basdif0  17018  tgval  17020  unitg  17032  tgdif0  17057  isopn2  17096  0cld  17102  ntropn  17113  ntrval2  17115  ntrdif  17116  clsdif  17117  cmclsopn  17126  cmntrcld  17127  clstop  17133  ntrtop  17134  cls0  17144  ntr0  17145  mretopd  17156  neips  17177  neiptopnei  17196  maxlp  17211  isperf2  17216  rest0  17233  iocpnfordt  17279  icomnfordt  17280  mnfnei  17285  bwth  17473  1stckgen  17586  ptbasfi  17613  pthaus  17670  imasnopn  17722  imasncld  17723  imasncls  17724  fbssfi  17869  isfil2  17888  ssfg  17904  filcon  17915  fbasrn  17916  filufint  17952  imaelfm  17983  fmfnfmlem4  17989  fclsfnflim  18059  alexsubALTlem3  18080  alexsubALTlem4  18081  ustfilxp  18242  ustuqtop1  18271  ustuqtop2  18272  ustuqtop3  18273  ustuqtop4  18274  utopsnneiplem  18277  utopsnnei  18279  utop2nei  18280  cfiluweak  18325  neipcfilu  18326  xmetres  18394  metres  18395  mopnex  18549  prdsms  18561  blval2  18605  metucnOLD  18618  metucn  18619  tngds  18689  nmoge0  18755  cnfldnm  18813  tgioo  18827  xrtgioo  18837  xrsmopn  18843  negcncf  18948  phtpy01  19010  pco0  19039  tchtopn  19184  tchnmfval  19186  caussi  19250  minveclem3b  19329  ovolfioo  19364  ovolficc  19365  ovolfsf  19368  ovolctb  19386  ovolctb2  19388  ovolfiniun  19397  ovoliun2  19402  ovolshftlem1  19405  ovolscalem1  19409  ovolicopnf  19420  iunmbl2  19451  uniioombllem2  19475  opnmblALT  19495  ismbf  19522  mbfinf  19557  0plef  19564  itg1climres  19606  itg2cnlem1  19653  iblitg  19660  ibl0  19678  itgcn  19734  cnlimc  19775  dvfre  19837  dvnfre  19838  dveflem  19863  dvef  19864  dvlipcn  19878  lhop2  19899  itgsubstlem  19932  evl1rhm  19949  ply1rem  20086  coefv0  20166  plyrecj  20197  vieta1lem2  20228  aannenlem1  20245  aaliou2b  20258  ulmval  20296  ulmpm  20299  ulmdvlem1  20316  mtest  20320  efcn  20359  sin2pim  20393  cos2pim  20394  sinmpi  20395  cosmpi  20396  sinppi  20397  cosppi  20398  efimpi  20399  sincosq1lem  20405  sincosq2sgn  20407  sincosq3sgn  20408  sincosq4sgn  20409  sinq12gt0  20415  sinq34lt0t  20417  sincosq1eq  20420  abssinper  20426  efif1o  20448  relogcn  20529  ellogdm  20530  efopn  20549  cxp0  20561  cxp1  20562  cxpsqr  20594  logsqr  20595  atandm3  20718  atanbnd  20766  atancn  20776  leibpi  20782  efrlim  20808  logdifbnd  20832  vmaprm  20900  ppip1le  20944  ppieq0  20959  prmorcht  20961  ppiublem1  20986  ppiub  20988  chpeq0  20992  chtub  20996  fsumvma  20997  pclogsum  20999  chpval2  21002  dchrresb  21043  dchrptlem1  21048  lgs0  21093  lgs2  21097  lgsdir2lem2  21108  lgsdir2lem4  21110  lgsdchrval  21131  lgsdchr  21132  lgseisenlem2  21134  dirith2  21222  selberg2lem  21244  qabvle  21319  qabvexp  21320  ostth  21333  uhgra0  21344  umgra0  21360  umisuhgra  21362  usisuslgra  21387  usgra0  21390  usgraedg4  21406  usgrafisbase  21428  usgrasscusgra  21492  uvtx01vtx  21501  fargshiftlem  21621  usgrcyclnl2  21628  constr3trl  21646  constr3pth  21647  constr3cycl  21648  4cycl4dv  21654  iseupa  21687  ex-po  21743  gx1  21850  addinv  21940  vcoprne  22058  nvnd  22180  ipval2lem3  22201  ipval2  22203  ipval2lem6  22207  4ipval3  22208  ipidsq  22209  dipcj  22213  dip0r  22216  nmlnogt0  22298  blocni  22306  ipasslem2  22333  ipasslem8  22338  ipasslem9  22339  ajval  22363  ubthlem1  22372  hvaddid2  22525  hvsub0  22578  hi02  22599  hlimi  22690  isch2  22726  chlimi  22737  chsupunss  22846  shsupunss  22848  chlejb1i  22978  h1dei  23052  h1de2ci  23058  spanunsni  23081  pjoml2i  23087  pjorthi  23171  mayete3i  23230  mayete3iOLD  23231  hosubid1  23301  nmopge0  23414  nmfnge0  23430  adj1  23436  adjeq  23438  lnop0  23469  lnopmi  23503  nmophmi  23534  cnlnadjlem5  23574  cnlnadjeui  23580  unierri  23607  leoprf2  23630  leopnmid  23641  nmopleid  23642  hstles  23734  hst0  23736  strlem3a  23755  dmdbr2  23806  mdsl1i  23824  mdsl2i  23825  mdsl2bi  23826  cvmdi  23827  mdslmd1lem1  23828  mdslmd1lem2  23829  mdslmd1i  23832  mdslmd2i  23833  csmdsymi  23837  mdexchi  23838  superpos  23857  atomli  23885  atordi  23887  chirredlem1  23893  chirredlem2  23894  atcvat4i  23900  atabsi  23904  mdsymlem1  23906  mdsymlem5  23910  mdsymlem6  23911  sumdmdii  23918  dmdbr5ati  23925  dmdbr6ati  23926  mddmdin0i  23934  cdj3lem2  23938  xppreima  24059  abfmpunirn  24064  abfmpel  24067  xlemnf  24117  xrdifh  24143  clatp0ex  24193  clatp1ex  24194  xrge0neqmnf  24212  metider  24289  rge0scvg  24335  lmxrge0  24337  qqh0  24368  qqh1  24369  zrhre  24385  rnlogblem  24399  logb1  24403  esumcst  24455  esumfzf  24459  esumfsupre  24461  hasheuni  24475  sgon  24507  dmvlsiga  24512  sigainb  24519  measval  24552  ismeas  24553  sxbrsigalem0  24621  rrvsum  24712  ballotlem2  24746  ballotlemfcc  24751  ballotlem4  24756  ptpcon  24920  cvmsss2  24961  cvmlift2lem12  25001  cvmlift2lem13  25002  cvmliftphtlem  25004  cvmliftpht  25005  relin01  25194  bcnm1  25201  fprod  25267  risefac0  25343  fallfac0  25344  risefac1  25349  fallfac1  25350  fprb  25397  opelco3  25403  predreseq  25454  predep  25467  trpred0  25514  wfr3g  25537  wfrlem14  25551  wfrlem15  25552  wlimeq1  25571  frr3g  25581  noxpsgn  25620  funpartfv  25790  imagesset  25798  altopeq1  25808  brbtwn  25838  colinearalglem4  25848  axlowdimlem13  25893  axlowdimlem17  25897  brcolinear2  25992  bpoly2  26103  bpoly3  26104  bpoly4  26105  fsumcube  26106  ontgval  26181  onint1  26199  mblfinlem1  26243  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  itg2addnclem  26256  itg2addnclem2  26257  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  ftc1anclem5  26284  ftc1anclem8  26287  gtinf  26322  cldbnd  26329  ivthALT  26338  refref  26365  refssfne  26374  tailfb  26406  unirep  26414  sdclem2  26446  totbndbnd  26498  heibor1lem  26518  heiborlem7  26526  bfplem1  26531  prnc  26677  fninfp  26735  fndifnfp  26737  fnnfpeq0  26739  ralxpmap  26742  mapfzcons1cl  26774  eldioph3b  26823  eldiophss  26833  0dioph  26837  vdioph  26838  eldioph4b  26872  eldioph4i  26873  rencldnfilem  26881  rmxy1  26985  rmxy0  26986  rmxm1  26997  rmym1  26998  monotoddzzfi  27005  nn0sqcl  27054  aomclem6  27134  pwslnmlem0  27170  pwslnmlem1  27171  isnumbasabl  27248  psgneldm2i  27405  seff  27515  lhe4.4ex1a  27523  fmuldfeqlem1  27688  fmuldfeq  27689  infrglb  27698  climneg  27712  stoweidlem18  27743  stoweidlem19  27744  stoweidlem22  27747  stoweidlem34  27759  stoweidlem40  27765  stoweidlem41  27766  stoweidlem55  27780  stoweidlem59  27784  rlimdmafv  28017  cnm1cn  28088  euhash1  28167  cshw0  28238  usgra2pthspth  28305  usgra2wlkspthlem2  28307  usgra2pthlem1  28310  el2wlkonotlem  28329  usg2wlkonot  28350  usg2wotspth  28351  frgrancvvdeqlemA  28426  eelT0  28887  snssl  28942  sineq0ALT  29049  bnj535  29261  bnj580  29284  bnj907  29336  bnj1253  29386  equs4NEW7  29533  lub0N  29987  glb0N  29991  glbconN  30174  atpointN  30540  polsubN  30704  pol0N  30706  pol1N  30707  2polvalN  30711  2polssN  30712  3polN  30713  pcl0N  30719  2pmaplubN  30723  pnonsingN  30730  polsubclN  30749  cdlemefs32sn1aw  31211  cdleme43fsv1snlem  31217  cdleme41sn3a  31230  cdleme32a  31238  cdleme40m  31264  cdleme40n  31265  cdleme42b  31275  istendo  31557  cdlemk40  31714  cdlemkid  31733  dihvalcqpre  32033
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