Theorem mpan 424

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mp2an  426  mpanl12  436  mp3an1  1358  mp3an12  1361  mp3an13  1362  ax9o  1744  sbnfc2  3185  ssdifss  3334  undifss  3572  uneqdifeqim  3577  elssuni  3916  csbexa  4213  difexg  4225  rabexg  4227  abssexg  4266  snexg  4268  copsexg  4330  sotritric  4415  sotritrieq  4416  trsuc  4513  oneli  4519  unexb  4533  opeluu  4541  rabxfr  4561  reuhyp  4563  ordunisuc2r  4606  reg3exmid  4672  brrelex12i  4761  brrelex1i  4762  brrelex2i  4763  xpss2  4830  opabid2  4853  eliunxp  4861  releldmi  4963  relelrni  4964  dmexg  4988  rnexg  4989  elres  5041  resexg  5045  relbrcnvg  5107  brcodir  5116  sotri  5124  sotri2  5126  sotri3  5127  dfrel2  5179  coi1  5244  fco  5491  fssres  5503  fabexg  5515  fvopab3g  5709  mptrcl  5719  mpteqb  5727  elfvmptrab1  5731  ffvelcdmi  5771  fsn2  5811  dfmptg  5816  fcof  5822  fvpr1  5847  fvconst2  5859  mptexg  5868  oprabid  6039  ovprc  6043  caovcl  6166  caovass  6172  caovdi  6191  elmpocl  6206  relmptopab  6213  ofexg  6229  resfunexgALT  6259  fo1stresm  6313  fo2ndresm  6314  1stexg  6319  2ndexg  6320  elopabi  6347  mpoexxg  6362  mpoxopn0yelv  6391  rntpos  6409  smores  6444  tfr0dm  6474  tfrlemibxssdm  6479  tfrexlem  6486  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  rdgruledefgg  6527  rdgruledefg  6528  rdgivallem  6533  rdgexg  6541  frec0g  6549  ordgt0ge1  6589  omfnex  6603  oeiv  6610  nna0r  6632  nnm0r  6633  nnsucsssuc  6646  nn2m  6681  nnaordex  6682  nnawordex  6683  ecdmn0m  6732  ecelqsi  6744  ecidg  6754  ectocl  6757  encv  6901  f1oen  6918  ssdomg  6938  map1  6973  fiprc  6976  dom1o  6985  xpdom1  7002  fict  7038  isinfinf  7067  ac6sfi  7068  xpfi  7105  en1eqsn  7126  fidcenumlemr  7133  fiss  7155  eqinfti  7198  djueq2  7219  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  djuf1olem  7231  djulclb  7233  inl11  7243  eldju1st  7249  1stinl  7252  2ndinl  7253  1stinr  7254  2ndinr  7255  ctssdccl  7289  isomnimap  7315  ismkvmap  7332  iswomnimap  7344  finacn  7397  djucomen  7409  exmidapne  7457  0nnq  7562  mulidnq  7587  archnqq  7615  prarloclemarch2  7617  nqnq0pi  7636  nq0m0r  7654  nq02m  7663  prarloclemlt  7691  prarloclemn  7697  prarloclem5  7698  addnqprllem  7725  addnqprulem  7726  appdivnq  7761  1idprl  7788  1idpru  7789  addextpr  7819  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemnbj  7865  caucvgprlemloc  7873  caucvgprprlemnbj  7891  caucvgprprlemloc  7901  caucvgprprlemaddq  7906  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemloc  7919  suplocexprlemlub  7922  0nsr  7947  ltsosr  7962  recexgt0sr  7971  prsrpos  7983  caucvgsr  8000  mappsrprg  8002  suplocsrlem  8006  mulresr  8036  axcnre  8079  axpre-ltwlin  8081  mullid  8155  0re  8157  axmulgt0  8229  ltnsym2  8248  eqlei  8251  ltnei  8261  muladd11  8290  cnegex  8335  0cnALT  8347  negcl  8357  negneg  8407  mul02  8544  mulm1  8557  lt0neg2  8627  le0neg2  8629  recexre  8736  recexgt0  8738  mulge0  8777  gt0ap0i  8785  recextlem1  8809  recexap  8811  recclapzi  8895  recap0apzi  8896  recidapzi  8897  divassapzi  8920  divmulapzi  8921  divdirapzi  8922  rerecclapzi  8934  ltp1  9002  recgt0i  9064  ltmul1i  9078  ltdiv1i  9079  ltmuldivi  9080  ltmul2i  9081  lemul1i  9082  lemul2i  9083  sup3exmid  9115  nngt1ne1  9156  nnrecre  9158  nn0ge0  9405  nn0addcl  9415  nn0mulcl  9416  zgt0ge1  9516  dfuzi  9568  eluzel2  9738  eluz2b1  9808  uz2m1nn  9812  elnn0dc  9818  elnndc  9819  nn01to3  9824  zq  9833  nnrecq  9852  rpge0  9874  rpreccl  9888  mnflt  9991  pnfnlt  9995  mnfle  10000  xrlelttr  10014  xrltletr  10015  xrletr  10016  xgepnf  10024  xlt0neg2  10047  xle0neg2  10049  xaddpnf2  10055  xaddmnf2  10057  xaddid2  10071  elioomnf  10176  ige3m2fz  10257  fzshftral  10316  ige2m1fz1  10317  1fv  10347  4fvwrd4  10348  rebtwn2zlemstep  10484  qbtwnxr  10489  btwnzge0  10532  zmodid2  10586  q2txmodxeq0  10618  frec2uzrand  10639  frecuzrdgtcl  10646  frecfzennn  10660  nn0ennn  10667  uzennn  10670  0exp  10808  sqgt0api  10859  subsq2  10881  qsqeqor  10884  bernneq  10894  faclbnd  10975  faclbnd2  10976  faclbnd3  10977  hashinfuni  11011  hashxp  11061  iswrdiz  11091  lsw0  11132  ccatlid  11154  s1leng  11172  s1fv  11174  s111  11179  pfx0g  11223  2shfti  11357  reim  11378  imcl  11380  crim  11384  caucvgre  11507  rennim  11528  resqrexlemdecn  11538  qabsor  11601  absimle  11610  sqrtthi  11645  sqrtcli  11646  sqrtgt0i  11647  sqrtmsqi  11648  sqrtsqi  11649  sqsqrti  11650  sqrtge0i  11651  absidi  11652  absnidi  11653  xrmaxiflemlub  11774  serclim0  11831  fsum2d  11961  fsumcnv  11963  fsumconst  11980  modfsummodlem1  11982  fsumabs  11991  binom11  12012  prodf1  12068  prodfclim1  12070  prodsnf  12118  fprod2d  12149  fprodcnv  12151  efzval  12209  eftlub  12216  efsep  12217  ef4p  12220  efgt1  12223  reef11  12225  sinf  12230  cosf  12231  efi4p  12243  sinneg  12252  cosneg  12253  efival  12258  efmival  12259  cos01gt0  12289  sin02gt0  12290  absefib  12297  efieq1re  12298  demoivre  12299  demoivreALT  12300  eirraplem  12303  0dvds  12337  odd2np1lem  12398  odd2np1  12399  even2n  12400  mod2eq0even  12404  2teven  12413  opoe  12421  omoe  12422  opeo  12423  omeo  12424  m1exp1  12427  bits0e  12475  bits0o  12476  bitsinv1  12488  gcd0id  12515  gcdid0  12516  1gcd  12528  lcmdvds  12616  isprm2lem  12653  isprm3  12655  prmgt1  12669  coprm  12681  isevengcd2  12695  isoddgcd1  12696  sqpweven  12712  2sqpwodd  12713  pythagtriplem12  12813  pythagtriplem13  12814  pythagtriplem14  12815  pythagtriplem16  12817  pc2dvds  12868  oddprmdvds  12892  pockthi  12896  1arith2  12906  unennn  12983  ctinfomlemom  13013  qnnen  13017  ssnnctlemct  13032  strslfv  13092  strle1g  13154  1strbas  13165  tgval  13310  ismgmn0  13406  mulgval  13674  mulgfng  13676  mulg0  13677  mulg1  13681  mulg2  13683  isnsg  13754  ringidvalg  13939  issrg  13943  subrgpropd  14232  rrgval  14241  islmod  14270  scaffvalg  14285  islssm  14336  sraval  14416  mopnset  14531  metuex  14534  zrhval  14596  zrhvalg  14597  zrhex  14600  psrbag  14648  istopon  14702  eltg4i  14744  eltg3  14746  tg1  14748  tg2  14749  topnex  14775  cldrcl  14791  restsn  14869  lmrcl  14881  metflem  15038  xmetf  15039  ismet2  15043  xmeteq0  15048  xmettri2  15050  xmetpsmet  15058  xmetres2  15068  blfvalps  15074  blex  15076  blvalps  15077  blval  15078  blfps  15098  blf  15099  mopnval  15131  cnbl0  15223  cnblcld  15224  blssioo  15242  resubmet  15245  cncfmet  15281  cnplimcim  15356  cnlimcim  15360  cnlimc  15361  dvfgg  15377  dvfpm  15378  dvfcnpm  15379  dvcj  15398  dvmptfsum  15414  reeff1olem  15460  ef2kpi  15495  sinperlem  15497  sin2kpi  15500  cos2kpi  15501  sinhalfpip  15509  sinhalfpim  15510  coshalfpip  15511  coshalfpim  15512  sincosq1sgn  15515  sinq12gt0  15519  sinkpi  15536  reeflog  15552  relogef  15553  logrpap0b  15565  loggt0b  15580  1cxp  15589  ecxp  15590  2logb9irrap  15666  0sgm  15674  lgsval2lem  15704  m1lgs  15779  1vgrex  15836  upgrfi  15917  umgredgnlp  15965  wlkop  16089  djucllem  16219  bdrabexg  16324  bdunexb  16338  peano5set  16358  speano5  16362  bj-omtrans  16374  pw1ninf  16414  pwf1oexmid  16424  nninfsellemeq  16440  iswomninnlem  16477