Theorem mpan2 707

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

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 |- ps
2	1	a1i 11	. 2 |- ( ph -> ps )
3		mpan2.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpdan 702	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mpanr12  721  mp3an23  1416  eueq2  3380  sbcgf  3501  sbcralg  3513  csbconstgf  3545  sbcnestg  3997  csbnestg  3998  csbnest1g  4001  mpteq1  4737  iinexg  4824  eusv2nf  4864  reusv2lem5  4873  nnullss  4930  xpss1  5228  xpiindi  5257  reldm0  5343  elrnmpt1s  5373  resdm  5441  resid  5460  eliniseg  5494  trinxp  5521  inimasn  5550  ssrnres  5572  cnveq0  5591  coi2  5652  relrelss  5659  cnviin  5672  predep  5706  ord0eln0  5779  funcnvres  5967  funimaex  5976  fnresin1  6005  fnresin2  6006  fresin  6073  dffv3  6187  ssimaex  6263  dmfco  6272  fvmpt  6282  fvmptnf  6302  fvimacnvALT  6336  dff3  6372  fsn  6402  fsn2  6403  funop  6414  fvrnressn  6428  fninfp  6440  fndifnfp  6442  fnnfpeq0  6444  elabrex  6501  f1elima  6520  fsnex  6538  fliftel1  6560  f1owe  6603  sorpssuni  6946  sorpssint  6947  eldifpw  6976  ordeleqon  6988  ordsson  6989  ssnlim  7083  2ndconst  7266  curry1  7269  tposfun  7368  tpostpos2  7373  wfr3g  7413  wfrlem14  7428  wfrlem15  7429  tfrlem10  7483  tfrlem12  7485  tfr3  7495  seqomlem1  7545  seqomlem2  7546  seqomlem4  7548  ondif2  7582  oa0  7596  om0  7597  oa1suc  7611  om1  7622  oe1  7624  oe1m  7625  omass  7660  oeoalem  7676  oeoelem  7678  nnmsucr  7705  nnm1  7728  nnm2  7729  ecelqsg  7802  xpider  7818  qsel  7826  mapdm0  7872  map0e  7895  fvdiagfn  7902  ralxpmap  7907  ixpsnf1o  7948  map1  8036  xp1en  8046  sbthlem7  8076  domunsn  8110  xpmapenlem  8127  infensuc  8138  infi  8184  finresfin  8186  diffi  8192  dif1en  8193  findcard2d  8202  unblem1  8212  unblem2  8213  unblem3  8214  unblem4  8215  isfinite2  8218  infn0  8222  unfilem1  8224  unfilem2  8225  unfir  8228  fofinf1o  8241  cnvfi  8248  pwfilem  8260  mptfi  8265  finsschain  8273  marypha2  8345  eqinf  8390  inf0  8518  trcl  8604  r1rankidb  8667  snwf  8672  unwf  8673  uniwf  8682  rankval3b  8689  rankr1a  8699  rankxplim3  8744  scott0  8749  card1  8794  pm54.43  8826  infxpenc2  8845  dfac8clem  8855  alephsuc2  8903  alephle  8911  cardaleph  8912  dfacacn  8963  dfac13  8964  dfac12lem2  8966  cdaval  8992  uncdadom  8993  cdaun  8994  cdacomen  9003  cdaassen  9004  cdadom1  9008  cdainf  9014  pwcda1  9016  ackbij1lem18  9059  cflem  9068  cflecard  9075  cfeq0  9078  cfslb  9088  cfsmolem  9092  cfcoflem  9094  cfidm  9097  isfin4-3  9137  fin23lem12  9153  fin23lem16  9157  fin23lem28  9162  fin23lem38  9171  fin23lem41  9174  fin1a2lem7  9228  fin1a2lem12  9233  fin1a2lem13  9234  hsmexlem8  9246  axcc2lem  9258  axcc3  9260  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  ac6num  9301  ttukeylem4  9334  ttukeylem7  9337  ttukey2g  9338  axdclem  9341  brdom3  9350  brdom5  9351  cardeq0  9374  unsnen  9375  konigthlem  9390  pwcfsdom  9405  canthp1lem1  9474  wunex2  9560  wuncval2  9569  eltsk2g  9573  intgru  9636  ingru  9637  grutsk  9644  axgroth6  9650  mulidpi  9708  nlt1pi  9728  indpi  9729  pinq  9749  mulidnq  9785  1idpr  9851  prlem934  9855  0idsr  9918  1idsr  9919  00sr  9920  negexsr  9923  recexsrlem  9924  sqgt0sr  9927  ax1rid  9982  axcnre  9985  ne0gt0  10142  peano2cn  10208  peano2re  10209  00id  10211  mul02lem2  10213  mul01  10215  subid  10300  subid1  10301  negid  10328  negeq0  10335  peano2cnm  10347  peano2rem  10348  lt0neg1  10534  le0neg1  10536  relin01  10552  div2neg  10748  recgt0ii  10929  divgt0i2i  10939  ledivp1i  10949  ltdivp1i  10950  peano5nni  11023  peano2nn  11032  nnge1  11046  times2  11146  addltmul  11268  nn0p1nn  11332  peano2nn0  11333  nn0lele2xi  11348  frnnn0fsupp  11350  peano2z  11418  peano2zm  11420  suprzcl  11457  zeo  11463  uzwo  11751  uzwo2  11752  infssuzle  11771  infssuzcl  11772  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  rphalfcl  11858  zgt1rpn0n1  11871  ltpnf  11954  nltmnf  11963  pnfge  11964  nltpnft  11995  xlemnf  11998  qsqueeze  12032  xlt0neg1  12050  xle0neg1  12052  xaddpnf1  12057  xaddmnf1  12059  xaddid1  12072  xsubge0  12091  xmul01  12097  xmulneg1  12099  xmulpnf1  12104  xmulid1  12109  supxrbnd  12158  supxrgtmnf  12159  supxrre1  12160  supxrre2  12161  elioopnf  12267  elicopnf  12269  xrge0neqmnf  12276  iccshftri  12307  iccshftli  12309  iccdili  12311  icccntri  12313  fzprval  12401  fz0add1fz1  12537  fzofzp1  12565  fzostep1  12584  injresinj  12589  flge0nn0  12621  flge1nn  12622  btwnzge0  12629  modfrac  12683  om2uzsuci  12747  axdc4uzlem  12782  ser1const  12857  exp0  12864  exp1  12866  expn1  12870  nn0sqcl  12887  expubnd  12921  sqval  12922  sqeq0  12927  resqcl  12931  zsqcl  12934  binom21  12980  expnbnd  12993  nn0opthlem2  13056  bcnn  13099  bcn2  13106  bcn2p1  13112  bcnm1  13114  hasheq0  13154  hashsng  13159  hashen1  13160  hashin  13199  hashdif  13201  hashxplem  13220  hashf1lem2  13240  hash2pr  13251  hash2prde  13252  pr2pwpr  13261  hash3tr  13272  iswrd  13307  wrdval  13308  wrdv  13320  ccatval2  13362  ccatrid  13370  s111  13395  swrd0len0  13436  repsw0  13524  repsw1  13530  cshw0  13540  wwlktovf  13699  relexpsucnnl  13772  shftfib  13812  reim0  13858  imval2  13891  cjne0  13903  abssq  14046  max0add  14050  abs2dif  14072  rddif  14080  absrdbnd  14081  rexuz3  14088  rlimdm  14282  isershft  14394  isercolllem2  14396  isercoll  14398  fsum  14451  fsumadd  14470  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  bcxmas  14567  infcvgaux2i  14590  fprod  14671  risefac0  14758  fallfac0  14759  risefac1  14764  fallfac1  14765  bpoly2  14788  bpoly3  14789  bpoly4  14790  fsumcube  14791  efi4p  14867  resin4p  14868  recos4p  14869  sinbnd  14910  cosbnd  14911  znnenlem  14940  rpnnen2lem8  14950  rpnnen2lem12  14954  cnso  14976  dvdsmul2  15004  dvdslelem  15031  odd2np1lem  15064  mod2eq1n2dvds  15071  divalglem0  15116  divalglem1  15117  divalglem4  15119  divalglem5  15120  divalglem8  15123  flodddiv4  15137  bits0  15150  bitsp1o  15155  bitsf1  15168  sadadd2lem2  15172  gcd1  15249  gcdmultiple  15269  lcm0val  15307  dvdslcm  15311  lcmeq0  15313  lcmgcd  15320  lcm1  15323  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  prm2orodd  15404  phiprm  15482  pc0  15559  pcdvdstr  15580  vdwlem2  15686  vdwlem6  15690  vdwlem8  15692  hashbc0  15709  setsval  15888  fsets  15891  setsres  15901  ressinbas  15936  ressress  15938  elrestr  16089  pwssnf1o  16158  xpsfrnel  16223  ismred2  16263  submre  16265  mreacs  16319  oppchomfval  16374  brssc  16474  isssc  16480  yonedalem4c  16917  isprs  16930  oduleval  17131  oduclatb  17144  gsumval2a  17279  mulg1  17548  mulgnegnn  17551  isghm  17660  ghmghmrn  17679  cntrnsg  17774  oppgplusfval  17778  psgneldm2i  17925  efgrelexlemb  18163  frgp0  18173  frgpmhm  18178  vrgpf  18181  cygctb  18293  dprd0  18430  dprd2da  18441  mgpplusg  18493  opprmulfval  18625  subrgint  18802  lsp0  19009  sralem  19177  rlmval2  19194  fczpsrbag  19367  ply1idvr1  19663  evls1rhmlem  19686  evl1fval1lem  19694  zringcyg  19839  mulgrhm2  19847  zlmsca  19869  chrnzr  19878  zrhpsgnelbas  19940  ocvz  20022  cssincl  20032  css0  20033  css1  20034  frlmip  20117  mat1scmat  20345  marrepeval  20369  decpmatid  20575  0opn  20709  topopn  20711  basdif0  20757  tgval  20759  isopn2  20836  0cld  20842  ntropn  20853  ntrval2  20855  ntrdif  20856  clsdif  20857  cmclsopn  20866  clstop  20873  ntrtop  20874  cls0  20884  ntr0  20885  mretopd  20896  neips  20917  neiptopnei  20936  maxlp  20951  isperf2  20956  rest0  20973  iocpnfordt  21019  icomnfordt  21020  mnfnei  21025  refref  21316  unisngl  21330  1stckgen  21357  ptbasfi  21384  pthaus  21441  imasnopn  21493  imasncld  21494  imasncls  21495  fbssfi  21641  isfil2  21660  ssfg  21676  filconn  21687  fbasrn  21688  filufint  21724  imaelfm  21755  fmfnfmlem4  21761  fclsfnflim  21831  alexsubALTlem3  21853  alexsubALTlem4  21854  ustfilxp  22016  ustuqtop1  22045  ustuqtop2  22046  ustuqtop3  22047  ustuqtop4  22048  utopsnneiplem  22051  utopsnnei  22053  utop2nei  22054  cfiluweak  22099  neipcfilu  22100  xmetres  22169  metres  22170  mopnex  22324  prdsms  22336  blval2  22367  metucn  22376  tngds  22452  tngngp3  22460  nmoge0  22525  cnfldnm  22582  tgioo  22599  xrtgioo  22609  xrsmopn  22615  negcncf  22721  phtpy01  22784  pco0  22814  tchtopn  23025  tchnmfval  23027  caussi  23095  rrxip  23178  minveclem3b  23199  ovolfioo  23236  ovolficc  23237  ovolfsf  23240  ovolctb  23258  ovolctb2  23260  ovolfiniun  23269  ovoliun2  23274  ovolshftlem1  23277  ovolscalem1  23281  ovolicopnf  23292  iunmbl2  23325  uniioombllem2  23351  opnmblALT  23371  ismbf  23397  mbfinf  23432  0plef  23439  itg1climres  23481  itg2cnlem1  23528  iblitg  23535  ibl0  23553  itgcn  23609  cnlimc  23652  dvfre  23714  dvnfre  23715  dveflem  23742  dvef  23743  dvlipcn  23757  lhop2  23778  itgsubstlem  23811  deg1val  23856  ply1rem  23923  coefv0  24004  plyrecj  24035  vieta1lem2  24066  aannenlem1  24083  aaliou2b  24096  ulmval  24134  ulmpm  24137  ulmdvlem1  24154  mtest  24158  efcn  24197  sin2pim  24237  cos2pim  24238  sinmpi  24239  cosmpi  24240  sinppi  24241  cosppi  24242  efimpi  24243  sincosq1lem  24249  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  sinq12gt0  24259  sinq34lt0t  24261  sincosq1eq  24264  abssinper  24270  efif1o  24292  loglt1b  24380  relogcn  24384  ellogdm  24385  efopn  24404  cxp0  24416  cxp1  24417  cxpsqrt  24449  logsqrt  24450  logb1  24507  atandm3  24605  atanbnd  24653  atancn  24663  leibpi  24669  efrlim  24696  logdifbnd  24720  vmaprm  24843  ppip1le  24887  ppieq0  24902  prmorcht  24904  ppiublem1  24927  ppiub  24929  chpeq0  24933  chtub  24937  fsumvma  24938  pclogsum  24940  chpval2  24943  dchrresb  24984  dchrptlem1  24989  lgs0  25035  lgs2  25039  lgsdir2lem2  25051  lgsdir2lem4  25053  lgsdchrval  25079  lgsdchr  25080  lgseisenlem2  25101  2lgslem1c  25118  2lgsoddprmlem2  25134  dirith2  25217  selberg2lem  25239  qabvle  25314  qabvexp  25315  ostth  25328  istrkg2ld  25359  ttgval  25755  cchhllem  25767  brbtwn  25779  colinearalglem4  25789  upgr0eop  26009  uspgrushgr  26070  usgruspgr  26073  usgr0eop  26138  0grsubgr  26170  dfnbgr2  26235  nbuhgr  26239  uspgrloopvtx  26411  umgr2v2evtx  26417  usgr0edg0rusgr  26471  rgrusgrprc  26485  wlkvtxiedg  26520  pthdivtx  26625  usgr2pthlem  26659  wlkpwwlkf1ouspgr  26765  wwlksext2clwwlk  26924  konigsbergssiedgw  27111  frgrncvvdeqlem7  27169  numclwwlk2lem1  27235  ex-po  27292  pliguhgr  27338  nvnd  27543  ipval2lem3  27560  ipval2  27562  ipidsq  27565  dipcj  27569  dip0r  27572  nmlnogt0  27652  blocni  27660  ipasslem2  27687  ipasslem8  27692  ipasslem9  27693  ajval  27717  ubthlem1  27726  hvaddid2  27880  hvsub0  27933  hi02  27954  hlimi  28045  isch2  28080  chlimi  28091  chsupunss  28203  shsupunss  28205  chlejb1i  28335  h1dei  28409  h1de2ci  28415  spanunsni  28438  pjoml2i  28444  pjorthi  28528  mayete3i  28587  hosubid1  28657  nmopge0  28770  nmfnge0  28786  adj1  28792  adjeq  28794  lnop0  28825  lnopmi  28859  nmophmi  28890  cnlnadjlem5  28930  cnlnadjeui  28936  unierri  28963  leoprf2  28986  leopnmid  28997  nmopleid  28998  hstles  29090  hst0  29092  strlem3a  29111  dmdbr2  29162  mdsl1i  29180  mdsl2i  29181  mdsl2bi  29182  cvmdi  29183  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd1i  29188  mdslmd2i  29189  csmdsymi  29193  mdexchi  29194  superpos  29213  atomli  29241  atordi  29243  chirredlem1  29249  chirredlem2  29250  atcvat4i  29256  atabsi  29260  mdsymlem1  29262  mdsymlem5  29266  mdsymlem6  29267  sumdmdii  29274  dmdbr5ati  29281  dmdbr6ati  29282  mddmdin0i  29290  cdj3lem2  29294  xppreima  29449  abfmpunirn  29452  abfmpel  29455  aciunf1lem  29462  fgreu  29471  imafi2  29489  padct  29497  fpwrelmapffslem  29507  fpwrelmap  29508  xrge0infss  29525  xrdifh  29542  clatp0cl  29671  clatp1cl  29672  resvval  29827  rearchi  29842  locfinreflem  29907  locfinref  29908  ordtconnlem1  29970  rge0scvg  29995  lmxrge0  29998  qqh0  30028  qqh1  30029  rrh0  30059  zrhre  30063  esumcst  30125  esumfzf  30131  esumfsupre  30133  hasheuni  30147  sgon  30187  dmvlsiga  30192  sigainb  30199  measval  30261  ismeas  30262  sxbrsigalem0  30333  omssubadd  30362  carsggect  30380  eulerpartlemmf  30437  eulerpartlemgs2  30442  eulerpartlemn  30443  rrvsum  30516  ballotlem2  30550  ballotlemfcc  30555  ballotlem4  30560  signsplypnf  30627  signsply0  30628  signsw0glem  30630  signswrid  30635  signlem0  30664  bnj535  30960  bnj580  30983  bnj907  31035  bnj1253  31085  ptpconn  31215  cvmsss2  31256  cvmlift2lem12  31296  cvmlift2lem13  31297  cvmliftphtlem  31299  cvmliftpht  31300  mppsthm  31476  bcneg1  31622  fprb  31669  opelco3  31678  fv1stcnv  31680  fv2ndcnv  31681  trpred0  31736  wlimeq1  31766  frr3g  31779  noextendseq  31820  noetalem3  31865  scutun12  31917  funpartfv  32052  imagesset  32060  altopeq1  32070  brcolinear2  32165  gtinfOLD  32314  cldbnd  32321  ivthALT  32330  refssfne  32353  tailfb  32372  ontgval  32430  onint1  32448  axc11n11r  32673  bj-restsn10  33039  bj-restsnid  33040  bj-rest10  33041  bj-rest0  33046  bj-inftyexpiinv  33095  bj-inftyexpidisj  33097  taupilem1  33167  f1omptsnlem  33183  mptsnunlem  33185  topdifinffinlem  33195  finixpnum  33394  tan2h  33401  matunitlindflem2  33406  ptrest  33408  poimirlem22  33431  poimirlem25  33434  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ftc1anclem5  33489  ftc1anclem8  33492  dvasin  33496  dvacos  33497  sdclem2  33538  totbndbnd  33588  heibor1lem  33608  heiborlem7  33616  bfplem1  33621  prnc  33866  el2v2  33986  riotasv  34245  glbconN  34663  atpointN  35029  polsubN  35193  pol0N  35195  pol1N  35196  2polvalN  35200  2polssN  35201  3polN  35202  pcl0N  35208  2pmaplubN  35212  pnonsingN  35219  polsubclN  35238  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme41sn3a  35721  cdleme32a  35729  cdleme40m  35755  cdleme40n  35756  cdleme42b  35766  istendo  36048  cdlemk40  36205  cdlemkid  36224  dihvalcqpre  36524  mapfzcons1cl  37281  eldioph3b  37328  eldiophss  37338  0dioph  37342  vdioph  37343  eldioph4b  37375  eldioph4i  37376  rencldnfilem  37384  rmxy1  37487  rmxy0  37488  rmxm1  37499  rmym1  37500  monotoddzzfi  37507  aomclem6  37629  pwslnmlem0  37661  pwslnmlem1  37662  isnumbasabl  37676  areaquad  37802  relexp2  37969  eltrclrec  37972  elrtrclrec  37973  brtrclrec  37988  brrtrclrec  37989  relexpxpmin  38009  dftrcl3  38012  dfrtrcl3  38025  heeq1  38071  seff  38508  lhe4.4ex1a  38528  eelT0  39002  snssl  39065  sineq0ALT  39173  elabrexg  39206  elrnmpt1sf  39376  founiiun0  39377  mapdm0OLD  39383  supxrgere  39549  supxrgelem  39553  fmuldfeqlem1  39814  fmuldfeq  39815  climneg  39842  sumnnodd  39862  liminfltlem  40036  addccncf2  40089  dvsinax  40127  stoweidlem18  40235  stoweidlem19  40236  stoweidlem22  40239  stoweidlem34  40251  stoweidlem40  40257  stoweidlem41  40258  stoweidlem55  40272  stoweidlem59  40276  dirker2re  40309  dirkerdenne0  40310  fourierdlem48  40371  fourierdlem49  40372  fourierdlem70  40393  fourierdlem71  40394  fourierdlem104  40427  fourierdlem112  40435  fouriersw  40448  etransclem46  40497  etransclem48  40499  nnfoctbdjlem  40672  rlimdmafv  41257  fsummmodsnunz  41345  flsqrt5  41509  bits0ALTV  41590  mogoldbblem  41629  sgoldbeven3prm  41671  nnsum3primes4  41676  uspgrsprfo  41756  2zrngnmlid  41949  2zrngnmrid  41950  mpt2exxg2  42116  lco0  42216  zlmodzxzldeplem3  42291  0dig1  42403  aacllem  42547