Theorem mpan 414

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  mp2an  416  mpanl12  426  mp3an1  1255  mp3an12  1258  mp3an13  1259  ax9o  1628  sbnfc2  2962  ssdifss  3102  undifss  3323  uneqdifeqim  3328  elssuni  3629  csbexa  3907  difexg  3919  rabexg  3921  abssexg  3955  snexg  3956  copsexg  3999  sotritric  4079  sotritrieq  4080  trsuc  4177  oneli  4183  unexb  4195  opeluu  4200  rabxfr  4220  reuhyp  4222  ordunisuc2r  4258  reg3exmid  4322  brrelexi  4402  brrelex2i  4403  xpss2  4467  opabid2  4485  eliunxp  4493  releldmi  4591  relelrni  4592  dmexg  4614  rnexg  4615  elres  4664  resexg  4668  relbrcnvg  4724  brcodir  4732  sotri  4740  sotri2  4742  sotri3  4743  dfrel2  4791  coi1  4856  fco  5076  fssres  5086  fabexg  5097  fvopab3g  5266  mpteqb  5282  ffvelrni  5322  fsn2  5358  dfmptg  5363  fvpr1  5386  fvconst2  5398  mptexg  5407  oprabid  5557  ovprc  5560  caovcl  5675  caovass  5681  caovdi  5700  elmpt2cl  5718  ofexg  5736  resfunexgALT  5757  fo1stresm  5808  fo2ndresm  5809  1stexg  5814  2ndexg  5815  elopabi  5841  mpt2exxg  5853  mpt2xopn0yelv  5877  rntpos  5895  smores  5930  tfr0  5960  tfrlemibxssdm  5964  tfrexlem  5971  rdgruledefgg  5985  rdgruledefg  5986  rdgivallem  5991  rdgon  5996  rdgexg  5999  frec0g  6006  ordgt0ge1  6041  omfnex  6052  oeiv  6059  oeicl  6065  nna0r  6080  nnm0r  6081  nnsucsssuc  6094  nn2m  6122  nnaordex  6123  nnawordex  6124  ecdmn0m  6171  ecelqsi  6183  ecidg  6193  ectocl  6196  encv  6250  f1oen  6262  ssdomg  6281  fiprc  6315  xpdom1  6332  ac6sfi  6379  eqinfti  6433  0nnq  6554  mulidnq  6579  archnqq  6607  prarloclemarch2  6609  nqnq0pi  6628  nq0m0r  6646  nq02m  6655  prarloclemlt  6683  prarloclemn  6689  prarloclem5  6690  addnqprllem  6717  addnqprulem  6718  appdivnq  6753  1idprl  6780  1idpru  6781  addextpr  6811  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemnbj  6857  caucvgprlemloc  6865  caucvgprprlemnbj  6883  caucvgprprlemloc  6893  caucvgprprlemaddq  6898  0nsr  6926  ltsosr  6941  recexgt0sr  6950  prsrpos  6961  caucvgsr  6978  mulresr  7006  axcnre  7047  axpre-ltwlin  7049  mulid2  7117  0re  7119  axmulgt0  7184  ltnsym2  7201  eqlei  7204  ltnei  7214  muladd11  7241  cnegex  7286  0cnALT  7298  negcl  7308  negneg  7358  mul02  7491  mulm1  7504  lt0neg2  7573  le0neg2  7575  recexre  7678  recexgt0  7680  mulge0  7719  gt0ap0i  7726  recextlem1  7741  recexap  7743  recclapzi  7825  recap0apzi  7826  recidapzi  7827  divassapzi  7850  divmulapzi  7851  divdirapzi  7852  rerecclapzi  7864  ltp1  7922  recgt0i  7984  ltmul1i  7998  ltdiv1i  7999  ltmuldivi  8000  ltmul2i  8001  lemul1i  8002  lemul2i  8003  nngt1ne1  8073  nnrecre  8075  nn0ge0  8313  nn0addcl  8323  nn0mulcl  8324  zgt0ge1  8409  dfuzi  8457  eluzel2  8624  eluz2b1  8688  uz2m1nn  8692  nn01to3  8702  zq  8711  nnrecq  8730  rpge0  8746  rpreccl  8760  mnflt  8858  pnfnlt  8862  mnfle  8867  xrlelttr  8876  xrltletr  8877  xrletr  8878  xlt0neg2  8906  xle0neg2  8908  elioomnf  8991  ige3m2fz  9068  fzshftral  9125  ige2m1fz1  9126  1fv  9149  4fvwrd4  9150  rebtwn2zlemstep  9261  qbtwnxr  9266  btwnzge0  9302  zmodid2  9354  q2txmodxeq0  9386  frec2uzrand  9407  frecuzrdgfn  9414  frecuzrdgsuc  9417  frecfzennn  9419  nn0ennn  9425  iseqeq4  9437  expival  9478  0exp  9511  sqgt0api  9561  subsq2  9582  bernneq  9593  faclbnd  9668  faclbnd2  9669  faclbnd3  9670  2shfti  9719  reim  9739  imcl  9741  crim  9745  caucvgre  9867  rennim  9888  resqrexlemdecn  9898  qabsor  9961  absimle  9970  sqrtthi  10005  sqrtcli  10006  sqrtgt0i  10007  sqrtmsqi  10008  sqrtsqi  10009  sqsqrti  10010  sqrtge0i  10011  absidi  10012  absnidi  10013  iserclim0  10144  0dvds  10215  odd2np1lem  10271  odd2np1  10272  even2n  10273  mod2eq0even  10277  2teven  10287  opoe  10295  omoe  10296  opeo  10297  omeo  10298  m1exp1  10301  gcd0id  10370  gcdid0  10371  1gcd  10383  lcmdvds  10461  isprm2lem  10498  isprm3  10500  prmgt1  10513  coprm  10523  isevengcd2  10537  isoddgcd1  10538  sqpweven  10553  2sqpwodd  10554  bdrabexg  10697  bdunexb  10711  peano5set  10735  speano5  10739  bj-omtrans  10751