Theorem mpan 416

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 414	1 |- ( ps -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  mp2an  418  mpanl12  428  mp3an1  1261  mp3an12  1264  mp3an13  1265  ax9o  1634  sbnfc2  2989  ssdifss  3131  undifss  3367  uneqdifeqim  3372  elssuni  3687  csbexa  3974  difexg  3986  rabexg  3988  abssexg  4023  snexg  4025  copsexg  4080  sotritric  4160  sotritrieq  4161  trsuc  4258  oneli  4264  unexb  4277  opeluu  4285  rabxfr  4305  reuhyp  4307  ordunisuc2r  4344  reg3exmid  4408  brrelex12i  4493  brrelex1i  4494  brrelex2i  4495  xpss2  4562  opabid2  4580  eliunxp  4588  releldmi  4687  relelrni  4688  dmexg  4710  rnexg  4711  elres  4761  resexg  4765  relbrcnvg  4824  brcodir  4832  sotri  4840  sotri2  4842  sotri3  4843  dfrel2  4894  coi1  4959  fco  5189  fssres  5199  fabexg  5211  fvopab3g  5390  mpteqb  5406  ffvelrni  5447  fsn2  5485  dfmptg  5490  fvpr1  5515  fvconst2  5527  mptexg  5536  oprabid  5695  ovprc  5698  caovcl  5813  caovass  5819  caovdi  5838  elmpt2cl  5856  ofexg  5874  resfunexgALT  5895  fo1stresm  5946  fo2ndresm  5947  1stexg  5952  2ndexg  5953  elopabi  5979  mpt2exxg  5991  mpt2xopn0yelv  6018  rntpos  6036  smores  6071  tfr0dm  6101  tfrlemibxssdm  6106  tfrexlem  6113  tfr1onlembxssdm  6122  tfrcllembxssdm  6135  rdgruledefgg  6154  rdgruledefg  6155  rdgivallem  6160  rdgexg  6168  frec0g  6176  ordgt0ge1  6213  omfnex  6224  oeiv  6231  nna0r  6253  nnm0r  6254  nnsucsssuc  6267  nn2m  6299  nnaordex  6300  nnawordex  6301  ecdmn0m  6348  ecelqsi  6360  ecidg  6370  ectocl  6373  encv  6517  f1oen  6530  ssdomg  6549  map1  6583  fiprc  6586  xpdom1  6605  fict  6638  isinfinf  6667  ac6sfi  6668  xpfi  6694  en1eqsn  6711  fidcenumlemr  6718  eqinfti  6769  djueq2  6788  djulclr  6795  djurclr  6796  djulcl  6797  djurcl  6798  djuf1olem  6799  djulclb  6801  djuun  6814  eldju1st  6816  1stinl  6819  2ndinl  6820  1stinr  6821  2ndinr  6822  isomnimap  6854  0nnq  6984  mulidnq  7009  archnqq  7037  prarloclemarch2  7039  nqnq0pi  7058  nq0m0r  7076  nq02m  7085  prarloclemlt  7113  prarloclemn  7119  prarloclem5  7120  addnqprllem  7147  addnqprulem  7148  appdivnq  7183  1idprl  7210  1idpru  7211  addextpr  7241  cauappcvgprlemdisj  7271  cauappcvgprlemloc  7272  cauappcvgprlemladdru  7276  cauappcvgprlemladdrl  7277  caucvgprlemnbj  7287  caucvgprlemloc  7295  caucvgprprlemnbj  7313  caucvgprprlemloc  7323  caucvgprprlemaddq  7328  0nsr  7356  ltsosr  7371  recexgt0sr  7380  prsrpos  7391  caucvgsr  7408  mulresr  7436  axcnre  7477  axpre-ltwlin  7479  mulid2  7547  0re  7549  axmulgt0  7619  ltnsym2  7636  eqlei  7639  ltnei  7649  muladd11  7676  cnegex  7721  0cnALT  7733  negcl  7743  negneg  7793  mul02  7926  mulm1  7939  lt0neg2  8008  le0neg2  8010  recexre  8116  recexgt0  8118  mulge0  8157  gt0ap0i  8164  recextlem1  8181  recexap  8183  recclapzi  8265  recap0apzi  8266  recidapzi  8267  divassapzi  8290  divmulapzi  8291  divdirapzi  8292  rerecclapzi  8304  ltp1  8366  recgt0i  8428  ltmul1i  8442  ltdiv1i  8443  ltmuldivi  8444  ltmul2i  8445  lemul1i  8446  lemul2i  8447  nngt1ne1  8518  nnrecre  8520  nn0ge0  8759  nn0addcl  8769  nn0mulcl  8770  zgt0ge1  8869  dfuzi  8917  eluzel2  9085  eluz2b1  9149  uz2m1nn  9153  nn01to3  9163  zq  9172  nnrecq  9191  rpge0  9207  rpreccl  9221  mnflt  9314  pnfnlt  9318  mnfle  9323  xrlelttr  9332  xrltletr  9333  xrletr  9334  xlt0neg2  9362  xle0neg2  9364  elioomnf  9447  ige3m2fz  9524  fzshftral  9583  ige2m1fz1  9584  1fv  9611  4fvwrd4  9612  rebtwn2zlemstep  9725  qbtwnxr  9730  btwnzge0  9768  zmodid2  9820  q2txmodxeq0  9852  frec2uzrand  9873  frecuzrdgtcl  9880  frecfzennn  9894  nn0ennn  9901  0exp  10051  sqgt0api  10101  subsq2  10123  bernneq  10135  faclbnd  10210  faclbnd2  10211  faclbnd3  10212  hashinfuni  10246  hashxp  10295  2shfti  10326  reim  10347  imcl  10349  crim  10353  caucvgre  10475  rennim  10496  resqrexlemdecn  10506  qabsor  10569  absimle  10578  sqrtthi  10613  sqrtcli  10614  sqrtgt0i  10615  sqrtmsqi  10616  sqrtsqi  10617  sqsqrti  10618  sqrtge0i  10619  absidi  10620  absnidi  10621  serclim0  10754  iserclim0  10755  fsum2d  10890  fsumcnv  10892  fsumconst  10909  modfsummodlem1  10911  fsumabs  10920  binom11  10941  efzval  11034  eftlub  11041  efsep  11042  ef4p  11045  efgt1  11048  reef11  11051  sinf  11056  cosf  11057  efi4p  11069  sinneg  11078  cosneg  11079  efival  11084  efmival  11085  cos01gt0  11114  sin02gt0  11115  absefib  11121  efieq1re  11122  demoivre  11123  demoivreALT  11124  eirraplem  11125  0dvds  11155  odd2np1lem  11211  odd2np1  11212  even2n  11213  mod2eq0even  11217  2teven  11226  opoe  11234  omoe  11235  opeo  11236  omeo  11237  m1exp1  11240  gcd0id  11309  gcdid0  11310  1gcd  11322  lcmdvds  11400  isprm2lem  11437  isprm3  11439  prmgt1  11452  coprm  11462  isevengcd2  11476  isoddgcd1  11477  sqpweven  11492  2sqpwodd  11493  unennn  11549  strslfv  11599  strle1g  11645  1strbas  11654  istopon  11773  tgval  11810  eltg4i  11816  eltg3  11818  tg1  11820  tg2  11821  topnex  11847  cldrcl  11863  djucllem  11973  bdrabexg  12070  bdunexb  12084  peano5set  12108  speano5  12112  bj-omtrans  12124  nninfsellemeq  12178