Theorem mpan 428

Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpan.1	|- ph
mpan.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpan	|- ( ps -> ch )

Proof of Theorem mpan

Step	Hyp	Ref	Expression
1		mpan.1	. . 3 |- ph
2	1	a1i 9	. 2 |- ( ps -> ph )
3		mpan.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpancom 426	1 |- ( ps -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mp2an  430  mpanl12  440  mp3an1  1365  mp3an12  1368  mp3an13  1369  ax9o  1750  sbnfc2  3208  ssdifss  3359  undifss  3608  uneqdifeqim  3613  elssuni  3963  csbexa  4264  difexg  4277  rabexg  4281  abssexg  4321  snexg  4323  copsexg  4386  sotritric  4471  sotritrieq  4472  trsuc  4569  oneli  4575  unexb  4590  opeluu  4598  rabxfr  4618  reuhyp  4620  ordunisuc2r  4663  reg3exmid  4729  brrelex12i  4819  brrelex1i  4820  brrelex2i  4821  xpss2  4888  opabid2  4913  eliunxp  4921  releldmi  5023  relelrni  5024  dmexg  5048  rnexg  5049  elres  5101  resexg  5105  relbrcnvg  5169  brcodir  5178  sotri  5186  sotri2  5188  sotri3  5189  dfrel2  5241  coi1  5306  fco  5555  fssres  5568  fabexg  5582  fvopab3g  5781  mptrcl  5791  mpteqb  5799  elfvmptrab1  5804  fvopab4ndm  5806  ffvelcdmi  5845  fsn2  5885  dfmptg  5891  fcof  5897  fvpr1  5922  fvconst2  5934  mptexg  5945  oprabid  6120  ovprc  6124  caovcl  6247  caovass  6253  caovdi  6272  elmpocl  6287  relmptopab  6294  ofexg  6310  resfunexgALT  6341  fo1stresm  6399  fo2ndresm  6400  1stexg  6405  2ndexg  6406  elopabi  6435  mpoexxg  6450  elmpom  6478  supp0  6482  mpoxopn0yelv  6515  rntpos  6533  smores  6568  tfr0dm  6598  tfrlemibxssdm  6603  tfrexlem  6610  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  rdgruledefgg  6651  rdgruledefg  6652  rdgivallem  6657  rdgexg  6665  frec0g  6673  ordgt0ge1  6713  omfnex  6727  oeiv  6734  nna0r  6756  nnm0r  6757  nnsucsssuc  6770  nn2m  6805  nnaordex  6806  nnawordex  6807  ecdmn0m  6856  ecelqsi  6868  ecidg  6878  ectocl  6881  mapfset  6950  encv  7034  f1oen  7051  ssdomg  7071  map1  7107  fiprc  7110  dom1o  7122  xpdom1  7139  fict  7176  isinfinf  7207  ac6sfi  7208  xpfi  7245  en1eqsn  7272  fidcenumlemr  7279  fiss  7316  fipwfi  7327  eqinfti  7366  djueq2  7387  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  djuf1olem  7399  djulclb  7401  inl11  7411  eldju1st  7417  1stinl  7420  2ndinl  7421  1stinr  7422  2ndinr  7423  ctssdccl  7457  isomnimap  7483  ismkvmap  7500  iswomnimap  7512  finacn  7566  djucomen  7578  exmidapne  7632  0nnq  7737  mulidnq  7762  archnqq  7790  prarloclemarch2  7792  nqnq0pi  7811  nq0m0r  7829  nq02m  7838  prarloclemlt  7866  prarloclemn  7872  prarloclem5  7873  addnqprllem  7900  addnqprulem  7901  appdivnq  7936  1idprl  7963  1idpru  7964  addextpr  7994  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemnbj  8040  caucvgprlemloc  8048  caucvgprprlemnbj  8066  caucvgprprlemloc  8076  caucvgprprlemaddq  8081  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemloc  8094  suplocexprlemlub  8097  0nsr  8122  ltsosr  8137  recexgt0sr  8146  prsrpos  8158  caucvgsr  8175  mappsrprg  8177  suplocsrlem  8181  mulresr  8211  axcnre  8254  axpre-ltwlin  8256  mullid  8330  0re  8332  axmulgt0  8403  ltnsym2  8422  eqlei  8426  ltnei  8436  muladd11  8466  cnegex  8511  0cnALT  8523  negcl  8533  negneg  8583  mul02  8721  mulm1  8734  lt0neg2  8804  le0neg2  8806  recexre  8914  recexgt0  8916  mulge0  8955  gt0ap0i  8963  recextlem1  8987  recexap  8989  recclapzi  9075  recap0apzi  9076  recidapzi  9077  divassapzi  9100  divmulapzi  9101  divdirapzi  9102  rerecclapzi  9114  ltp1  9182  recgt0i  9244  ltmul1i  9258  ltdiv1i  9259  ltmuldivi  9260  ltmul2i  9261  lemul1i  9262  lemul2i  9263  sup3exmid  9295  nngt1ne1  9348  nnrecre  9350  nn0ge0  9599  nn0addcl  9609  nn0mulcl  9610  zgt0ge1  9712  dfuzi  9766  eluzel2  9941  eluz2b1  10016  uz2m1nn  10020  elnn0dc  10026  elnndc  10027  nn01to3  10032  zq  10041  nnrecq  10060  rpge0  10083  rpreccl  10097  mnflt  10201  pnfnlt  10205  mnfle  10210  xrlelttr  10224  xrltletr  10225  xrletr  10226  xgepnf  10234  xlt0neg2  10257  xle0neg2  10259  xaddpnf2  10265  xaddmnf2  10267  xaddid2  10281  elioomnf  10386  ige3m2fz  10470  fzshftral  10531  ige2m1fz1  10532  1fv  10562  4fvwrd4  10563  rebtwn2zlemstep  10703  qbtwnxr  10708  btwnzge0  10755  zmodid2  10809  q2txmodxeq0  10841  frec2uzrand  10862  frecuzrdgtcl  10869  frecfzennn  10883  nn0ennn  10890  uzennn  10893  0exp  11031  sqgt0api  11082  subsq2  11104  qsqeqor  11107  bernneq  11118  faclbnd  11200  faclbnd2  11201  faclbnd3  11202  hashinfuni  11237  hashxp  11288  hashpwfi  11290  iswrdiz  11332  lsw0  11373  ccatlid  11395  s1leng  11413  s1fv  11415  s111  11420  pfx0g  11469  2shfti  11617  reim  11638  imcl  11640  crim  11644  caucvgre  11768  rennim  11789  resqrexlemdecn  11799  qabsor  11862  absimle  11872  sqrtthi  11907  sqrtcli  11908  sqrtgt0i  11909  sqrtmsqi  11910  sqrtsqi  11911  sqsqrti  11912  sqrtge0i  11913  absidi  11914  absnidi  11915  xrmaxiflemlub  12038  serclim0  12095  fsum2d  12226  fsumcnv  12228  fsumconst  12245  modfsummodlem1  12247  fsumabs  12256  binom11  12277  prodf1  12333  prodfclim1  12335  prodsnf  12383  fprod2d  12414  fprodcnv  12416  efzval  12474  eftlub  12481  efsep  12482  ef4p  12485  efgt1  12488  reef11  12490  sinf  12495  cosf  12496  efi4p  12508  sinneg  12517  cosneg  12518  efival  12523  efmival  12524  cos01gt0  12554  sin02gt0  12555  absefib  12562  efieq1re  12563  demoivre  12564  demoivreALT  12565  eirraplem  12568  0dvds  12602  odd2np1lem  12663  odd2np1  12664  even2n  12665  mod2eq0even  12669  2teven  12678  opoe  12686  omoe  12687  opeo  12688  omeo  12689  m1exp1  12692  bits0e  12740  bits0o  12741  bitsinv1  12753  gcd0id  12780  gcdid0  12781  1gcd  12793  lcmdvds  12881  isprm2lem  12918  isprm3  12920  prmgt1  12935  coprm  12947  isevengcd2  12961  isoddgcd1  12962  sqpweven  12979  2sqpwodd  12980  sqrtrirr  13013  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem14  13084  pythagtriplem16  13086  pc2dvds  13137  oddprmdvds  13161  pockthi  13165  1arith2  13175  prmlem1a  13249  unennn  13345  ctinfomlemom  13375  qnnen  13379  ssnnctlemct  13394  strslfv  13454  slotm  13472  strle1g  13518  1strbas  13529  tgval  13674  ismgmn0  13736  mulgval  13983  mulgfng  13985  mulg0  13986  mulg1  13990  mulg2  13992  isnsg  14063  cntrval  14150  mgpplusg  14328  mgpbas  14331  ringidvalg  14370  ringidval  14371  issrg  14375  subrgpropd  14669  rrgval  14678  islmod  14735  scaffvalg  14751  islssm  14802  sraval  14882  mopnset  14997  metuex  15000  zrhval  15060  zrhvalg  15061  zrhex  15064  asclfval  15129  psrbag  15163  psrbagaddclfi  15173  istopon  15256  eltg4i  15298  eltg3  15300  tg1  15302  tg2  15303  topnex  15329  cldrcl  15345  restsn  15423  lmrcl  15435  metflem  15592  xmetf  15593  ismet2  15597  xmeteq0  15602  xmettri2  15604  xmetpsmet  15612  xmetres2  15622  blfvalps  15628  blex  15630  blvalps  15631  blval  15632  blfps  15652  blf  15653  mopnval  15685  cnbl0  15777  cnblcld  15778  blssioo  15796  resubmet  15799  cncfmet  15835  cnplimcim  15910  cnlimcim  15914  cnlimc  15915  dvfgg  15931  dvfpm  15932  dvfcnpm  15933  dvcj  15952  dvmptfsum  15968  reeff1olem  16014  ef2kpi  16050  sinperlem  16052  sin2kpi  16055  cos2kpi  16056  sinhalfpip  16064  sinhalfpim  16065  coshalfpip  16066  coshalfpim  16067  sincosq1sgn  16070  sinq12gt0  16074  sinkpi  16091  sineq0re  16093  reeflog  16109  relogef  16110  logrpap0b  16123  loggt0b  16138  1cxp  16150  ecxp  16151  2logb9irrap  16230  log2tlbndlog2  16237  log2ublem2  16239  0sgm  16271  chtublem  16312  pcbcctr  16320  bcp1ctr  16323  bclbnd  16324  bposlem1  16328  lgsval2lem  16351  m1lgs  16426  1vgrex  16483  upgrfi  16565  umgredgnlp  16615  wlkop  16811  clwwlkn0  16871  djucllem  17050  bdrabexg  17154  bdunexb  17168  peano5set  17188  speano5  17192  bj-omtrans  17204  pw1ninf  17243  pwf1oexmid  17251  nninfsellemeq  17280  iswomninnlem  17323