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  4262  difexg  4275  rabexg  4279  abssexg  4319  snexg  4321  copsexg  4384  sotritric  4469  sotritrieq  4470  trsuc  4567  oneli  4573  unexb  4588  opeluu  4596  rabxfr  4616  reuhyp  4618  ordunisuc2r  4661  reg3exmid  4727  brrelex12i  4817  brrelex1i  4818  brrelex2i  4819  xpss2  4886  opabid2  4911  eliunxp  4919  releldmi  5021  relelrni  5022  dmexg  5046  rnexg  5047  elres  5099  resexg  5103  relbrcnvg  5166  brcodir  5175  sotri  5183  sotri2  5185  sotri3  5186  dfrel2  5238  coi1  5303  fco  5552  fssres  5565  fabexg  5579  fvopab3g  5778  mptrcl  5788  mpteqb  5796  elfvmptrab1  5801  fvopab4ndm  5803  ffvelcdmi  5842  fsn2  5882  dfmptg  5888  fcof  5894  fvpr1  5919  fvconst2  5931  mptexg  5942  oprabid  6117  ovprc  6121  caovcl  6244  caovass  6250  caovdi  6269  elmpocl  6284  relmptopab  6291  ofexg  6307  resfunexgALT  6337  fo1stresm  6395  fo2ndresm  6396  1stexg  6401  2ndexg  6402  elopabi  6431  mpoexxg  6446  elmpom  6474  supp0  6478  mpoxopn0yelv  6510  rntpos  6528  smores  6563  tfr0dm  6593  tfrlemibxssdm  6598  tfrexlem  6605  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  rdgruledefgg  6646  rdgruledefg  6647  rdgivallem  6652  rdgexg  6660  frec0g  6668  ordgt0ge1  6708  omfnex  6722  oeiv  6729  nna0r  6751  nnm0r  6752  nnsucsssuc  6765  nn2m  6800  nnaordex  6801  nnawordex  6802  ecdmn0m  6851  ecelqsi  6863  ecidg  6873  ectocl  6876  mapfset  6945  encv  7028  f1oen  7045  ssdomg  7065  map1  7101  fiprc  7104  dom1o  7116  xpdom1  7133  fict  7170  isinfinf  7201  ac6sfi  7202  xpfi  7239  en1eqsn  7265  fidcenumlemr  7272  fiss  7311  fipwfi  7321  eqinfti  7360  djueq2  7381  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  djuf1olem  7393  djulclb  7395  inl11  7405  eldju1st  7411  1stinl  7414  2ndinl  7415  1stinr  7416  2ndinr  7417  ctssdccl  7451  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  finacn  7560  djucomen  7572  exmidapne  7626  0nnq  7731  mulidnq  7756  archnqq  7784  prarloclemarch2  7786  nqnq0pi  7805  nq0m0r  7823  nq02m  7832  prarloclemlt  7860  prarloclemn  7866  prarloclem5  7867  addnqprllem  7894  addnqprulem  7895  appdivnq  7930  1idprl  7957  1idpru  7958  addextpr  7988  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemnbj  8034  caucvgprlemloc  8042  caucvgprprlemnbj  8060  caucvgprprlemloc  8070  caucvgprprlemaddq  8075  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemloc  8088  suplocexprlemlub  8091  0nsr  8116  ltsosr  8131  recexgt0sr  8140  prsrpos  8152  caucvgsr  8169  mappsrprg  8171  suplocsrlem  8175  mulresr  8205  axcnre  8248  axpre-ltwlin  8250  mullid  8324  0re  8326  axmulgt0  8397  ltnsym2  8416  eqlei  8419  ltnei  8429  muladd11  8459  cnegex  8504  0cnALT  8516  negcl  8526  negneg  8576  mul02  8714  mulm1  8727  lt0neg2  8797  le0neg2  8799  recexre  8906  recexgt0  8908  mulge0  8947  gt0ap0i  8955  recextlem1  8979  recexap  8981  recclapzi  9067  recap0apzi  9068  recidapzi  9069  divassapzi  9092  divmulapzi  9093  divdirapzi  9094  rerecclapzi  9106  ltp1  9174  recgt0i  9236  ltmul1i  9250  ltdiv1i  9251  ltmuldivi  9252  ltmul2i  9253  lemul1i  9254  lemul2i  9255  sup3exmid  9287  nngt1ne1  9339  nnrecre  9341  nn0ge0  9588  nn0addcl  9598  nn0mulcl  9599  zgt0ge1  9703  dfuzi  9756  eluzel2  9926  eluz2b1  10001  uz2m1nn  10005  elnn0dc  10011  elnndc  10012  nn01to3  10017  zq  10026  nnrecq  10045  rpge0  10067  rpreccl  10081  mnflt  10185  pnfnlt  10189  mnfle  10194  xrlelttr  10208  xrltletr  10209  xrletr  10210  xgepnf  10218  xlt0neg2  10241  xle0neg2  10243  xaddpnf2  10249  xaddmnf2  10251  xaddid2  10265  elioomnf  10370  ige3m2fz  10454  fzshftral  10515  ige2m1fz1  10516  1fv  10546  4fvwrd4  10547  rebtwn2zlemstep  10687  qbtwnxr  10692  btwnzge0  10735  zmodid2  10789  q2txmodxeq0  10821  frec2uzrand  10842  frecuzrdgtcl  10849  frecfzennn  10863  nn0ennn  10870  uzennn  10873  0exp  11011  sqgt0api  11062  subsq2  11084  qsqeqor  11087  bernneq  11098  faclbnd  11179  faclbnd2  11180  faclbnd3  11181  hashinfuni  11216  hashxp  11267  hashpwfi  11269  iswrdiz  11311  lsw0  11352  ccatlid  11374  s1leng  11392  s1fv  11394  s111  11399  pfx0g  11448  2shfti  11596  reim  11617  imcl  11619  crim  11623  caucvgre  11747  rennim  11768  resqrexlemdecn  11778  qabsor  11841  absimle  11850  sqrtthi  11885  sqrtcli  11886  sqrtgt0i  11887  sqrtmsqi  11888  sqrtsqi  11889  sqsqrti  11890  sqrtge0i  11891  absidi  11892  absnidi  11893  xrmaxiflemlub  12014  serclim0  12071  fsum2d  12202  fsumcnv  12204  fsumconst  12221  modfsummodlem1  12223  fsumabs  12232  binom11  12253  prodf1  12309  prodfclim1  12311  prodsnf  12359  fprod2d  12390  fprodcnv  12392  efzval  12450  eftlub  12457  efsep  12458  ef4p  12461  efgt1  12464  reef11  12466  sinf  12471  cosf  12472  efi4p  12484  sinneg  12493  cosneg  12494  efival  12499  efmival  12500  cos01gt0  12530  sin02gt0  12531  absefib  12538  efieq1re  12539  demoivre  12540  demoivreALT  12541  eirraplem  12544  0dvds  12578  odd2np1lem  12639  odd2np1  12640  even2n  12641  mod2eq0even  12645  2teven  12654  opoe  12662  omoe  12663  opeo  12664  omeo  12665  m1exp1  12668  bits0e  12716  bits0o  12717  bitsinv1  12729  gcd0id  12756  gcdid0  12757  1gcd  12769  lcmdvds  12857  isprm2lem  12894  isprm3  12896  prmgt1  12910  coprm  12922  isevengcd2  12936  isoddgcd1  12937  sqpweven  12953  2sqpwodd  12954  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem14  13056  pythagtriplem16  13058  pc2dvds  13109  oddprmdvds  13133  pockthi  13137  1arith2  13147  unennn  13288  ctinfomlemom  13318  qnnen  13322  ssnnctlemct  13337  strslfv  13397  slotm  13415  strle1g  13460  1strbas  13471  tgval  13616  ismgmn0  13678  mulgval  13925  mulgfng  13927  mulg0  13928  mulg1  13932  mulg2  13934  isnsg  14005  mgpplusg  14222  mgpbas  14225  ringidvalg  14264  ringidval  14265  issrg  14269  subrgpropd  14561  rrgval  14570  islmod  14627  scaffvalg  14643  islssm  14694  sraval  14774  mopnset  14889  metuex  14892  zrhval  14952  zrhvalg  14953  zrhex  14956  asclfval  15021  psrbag  15053  psrbagaddclfi  15061  istopon  15114  eltg4i  15156  eltg3  15158  tg1  15160  tg2  15161  topnex  15187  cldrcl  15203  restsn  15281  lmrcl  15293  metflem  15450  xmetf  15451  ismet2  15455  xmeteq0  15460  xmettri2  15462  xmetpsmet  15470  xmetres2  15480  blfvalps  15486  blex  15488  blvalps  15489  blval  15490  blfps  15510  blf  15511  mopnval  15543  cnbl0  15635  cnblcld  15636  blssioo  15654  resubmet  15657  cncfmet  15693  cnplimcim  15768  cnlimcim  15772  cnlimc  15773  dvfgg  15789  dvfpm  15790  dvfcnpm  15791  dvcj  15810  dvmptfsum  15826  reeff1olem  15872  ef2kpi  15907  sinperlem  15909  sin2kpi  15912  cos2kpi  15913  sinhalfpip  15921  sinhalfpim  15922  coshalfpip  15923  coshalfpim  15924  sincosq1sgn  15927  sinq12gt0  15931  sinkpi  15948  reeflog  15964  relogef  15965  logrpap0b  15977  loggt0b  15992  1cxp  16002  ecxp  16003  2logb9irrap  16079  log2tlbndlog2  16082  log2ublem2  16084  0sgm  16099  lgsval2lem  16129  m1lgs  16204  1vgrex  16261  upgrfi  16343  umgredgnlp  16393  wlkop  16589  clwwlkn0  16649  djucllem  16828  bdrabexg  16932  bdunexb  16946  peano5set  16966  speano5  16970  bj-omtrans  16982  pw1ninf  17021  pwf1oexmid  17029  nninfsellemeq  17057  iswomninnlem  17099