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  1337  mp3an12  1340  mp3an13  1341  ax9o  1721  sbnfc2  3154  ssdifss  3303  undifss  3541  uneqdifeqim  3546  elssuni  3878  csbexa  4173  difexg  4185  rabexg  4187  abssexg  4226  snexg  4228  copsexg  4288  sotritric  4371  sotritrieq  4372  trsuc  4469  oneli  4475  unexb  4489  opeluu  4497  rabxfr  4517  reuhyp  4519  ordunisuc2r  4562  reg3exmid  4628  brrelex12i  4717  brrelex1i  4718  brrelex2i  4719  xpss2  4786  opabid2  4809  eliunxp  4817  releldmi  4917  relelrni  4918  dmexg  4942  rnexg  4943  elres  4995  resexg  4999  relbrcnvg  5061  brcodir  5070  sotri  5078  sotri2  5080  sotri3  5081  dfrel2  5133  coi1  5198  fco  5441  fssres  5451  fabexg  5463  fvopab3g  5652  mptrcl  5662  mpteqb  5670  elfvmptrab1  5674  ffvelcdmi  5714  fsn2  5754  dfmptg  5759  fvpr1  5788  fvconst2  5800  mptexg  5809  oprabid  5976  ovprc  5980  caovcl  6101  caovass  6107  caovdi  6126  elmpocl  6141  ofexg  6163  resfunexgALT  6193  fo1stresm  6247  fo2ndresm  6248  1stexg  6253  2ndexg  6254  elopabi  6281  mpoexxg  6296  mpoxopn0yelv  6325  rntpos  6343  smores  6378  tfr0dm  6408  tfrlemibxssdm  6413  tfrexlem  6420  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  rdgruledefgg  6461  rdgruledefg  6462  rdgivallem  6467  rdgexg  6475  frec0g  6483  ordgt0ge1  6521  omfnex  6535  oeiv  6542  nna0r  6564  nnm0r  6565  nnsucsssuc  6578  nn2m  6613  nnaordex  6614  nnawordex  6615  ecdmn0m  6664  ecelqsi  6676  ecidg  6686  ectocl  6689  encv  6833  f1oen  6850  ssdomg  6870  map1  6904  fiprc  6907  xpdom1  6930  fict  6965  isinfinf  6994  ac6sfi  6995  xpfi  7029  en1eqsn  7050  fidcenumlemr  7057  fiss  7079  eqinfti  7122  djueq2  7143  djulclr  7151  djurclr  7152  djulcl  7153  djurcl  7154  djuf1olem  7155  djulclb  7157  inl11  7167  eldju1st  7173  1stinl  7176  2ndinl  7177  1stinr  7178  2ndinr  7179  ctssdccl  7213  isomnimap  7239  ismkvmap  7256  iswomnimap  7268  finacn  7316  djucomen  7328  exmidapne  7372  0nnq  7477  mulidnq  7502  archnqq  7530  prarloclemarch2  7532  nqnq0pi  7551  nq0m0r  7569  nq02m  7578  prarloclemlt  7606  prarloclemn  7612  prarloclem5  7613  addnqprllem  7640  addnqprulem  7641  appdivnq  7676  1idprl  7703  1idpru  7704  addextpr  7734  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemnbj  7780  caucvgprlemloc  7788  caucvgprprlemnbj  7806  caucvgprprlemloc  7816  caucvgprprlemaddq  7821  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemloc  7834  suplocexprlemlub  7837  0nsr  7862  ltsosr  7877  recexgt0sr  7886  prsrpos  7898  caucvgsr  7915  mappsrprg  7917  suplocsrlem  7921  mulresr  7951  axcnre  7994  axpre-ltwlin  7996  mullid  8070  0re  8072  axmulgt0  8144  ltnsym2  8163  eqlei  8166  ltnei  8176  muladd11  8205  cnegex  8250  0cnALT  8262  negcl  8272  negneg  8322  mul02  8459  mulm1  8472  lt0neg2  8542  le0neg2  8544  recexre  8651  recexgt0  8653  mulge0  8692  gt0ap0i  8700  recextlem1  8724  recexap  8726  recclapzi  8810  recap0apzi  8811  recidapzi  8812  divassapzi  8835  divmulapzi  8836  divdirapzi  8837  rerecclapzi  8849  ltp1  8917  recgt0i  8979  ltmul1i  8993  ltdiv1i  8994  ltmuldivi  8995  ltmul2i  8996  lemul1i  8997  lemul2i  8998  sup3exmid  9030  nngt1ne1  9071  nnrecre  9073  nn0ge0  9320  nn0addcl  9330  nn0mulcl  9331  zgt0ge1  9431  dfuzi  9483  eluzel2  9653  eluz2b1  9722  uz2m1nn  9726  elnn0dc  9732  elnndc  9733  nn01to3  9738  zq  9747  nnrecq  9766  rpge0  9788  rpreccl  9802  mnflt  9905  pnfnlt  9909  mnfle  9914  xrlelttr  9928  xrltletr  9929  xrletr  9930  xgepnf  9938  xlt0neg2  9961  xle0neg2  9963  xaddpnf2  9969  xaddmnf2  9971  xaddid2  9985  elioomnf  10090  ige3m2fz  10171  fzshftral  10230  ige2m1fz1  10231  1fv  10261  4fvwrd4  10262  rebtwn2zlemstep  10395  qbtwnxr  10400  btwnzge0  10443  zmodid2  10497  q2txmodxeq0  10529  frec2uzrand  10550  frecuzrdgtcl  10557  frecfzennn  10571  nn0ennn  10578  uzennn  10581  0exp  10719  sqgt0api  10770  subsq2  10792  qsqeqor  10795  bernneq  10805  faclbnd  10886  faclbnd2  10887  faclbnd3  10888  hashinfuni  10922  hashxp  10971  iswrdiz  11001  lsw0  11041  ccatlid  11062  s1leng  11078  s1fv  11080  s111  11085  2shfti  11142  reim  11163  imcl  11165  crim  11169  caucvgre  11292  rennim  11313  resqrexlemdecn  11323  qabsor  11386  absimle  11395  sqrtthi  11430  sqrtcli  11431  sqrtgt0i  11432  sqrtmsqi  11433  sqrtsqi  11434  sqsqrti  11435  sqrtge0i  11436  absidi  11437  absnidi  11438  xrmaxiflemlub  11559  serclim0  11616  fsum2d  11746  fsumcnv  11748  fsumconst  11765  modfsummodlem1  11767  fsumabs  11776  binom11  11797  prodf1  11853  prodfclim1  11855  prodsnf  11903  fprod2d  11934  fprodcnv  11936  efzval  11994  eftlub  12001  efsep  12002  ef4p  12005  efgt1  12008  reef11  12010  sinf  12015  cosf  12016  efi4p  12028  sinneg  12037  cosneg  12038  efival  12043  efmival  12044  cos01gt0  12074  sin02gt0  12075  absefib  12082  efieq1re  12083  demoivre  12084  demoivreALT  12085  eirraplem  12088  0dvds  12122  odd2np1lem  12183  odd2np1  12184  even2n  12185  mod2eq0even  12189  2teven  12198  opoe  12206  omoe  12207  opeo  12208  omeo  12209  m1exp1  12212  bits0e  12260  bits0o  12261  bitsinv1  12273  gcd0id  12300  gcdid0  12301  1gcd  12313  lcmdvds  12401  isprm2lem  12438  isprm3  12440  prmgt1  12454  coprm  12466  isevengcd2  12480  isoddgcd1  12481  sqpweven  12497  2sqpwodd  12498  pythagtriplem12  12598  pythagtriplem13  12599  pythagtriplem14  12600  pythagtriplem16  12602  pc2dvds  12653  oddprmdvds  12677  pockthi  12681  1arith2  12691  unennn  12768  ctinfomlemom  12798  qnnen  12802  ssnnctlemct  12817  strslfv  12877  strle1g  12938  1strbas  12949  tgval  13094  ismgmn0  13190  mulgval  13458  mulgfng  13460  mulg0  13461  mulg1  13465  mulg2  13467  isnsg  13538  ringidvalg  13723  issrg  13727  subrgpropd  14015  rrgval  14024  islmod  14053  scaffvalg  14068  islssm  14119  sraval  14199  mopnset  14314  metuex  14317  zrhval  14379  zrhvalg  14380  zrhex  14383  psrbag  14431  istopon  14485  eltg4i  14527  eltg3  14529  tg1  14531  tg2  14532  topnex  14558  cldrcl  14574  restsn  14652  lmrcl  14663  metflem  14821  xmetf  14822  ismet2  14826  xmeteq0  14831  xmettri2  14833  xmetpsmet  14841  xmetres2  14851  blfvalps  14857  blex  14859  blvalps  14860  blval  14861  blfps  14881  blf  14882  mopnval  14914  cnbl0  15006  cnblcld  15007  blssioo  15025  resubmet  15028  cncfmet  15064  cnplimcim  15139  cnlimcim  15143  cnlimc  15144  dvfgg  15160  dvfpm  15161  dvfcnpm  15162  dvcj  15181  dvmptfsum  15197  reeff1olem  15243  ef2kpi  15278  sinperlem  15280  sin2kpi  15283  cos2kpi  15284  sinhalfpip  15292  sinhalfpim  15293  coshalfpip  15294  coshalfpim  15295  sincosq1sgn  15298  sinq12gt0  15302  sinkpi  15319  reeflog  15335  relogef  15336  logrpap0b  15348  loggt0b  15363  1cxp  15372  ecxp  15373  2logb9irrap  15449  0sgm  15457  lgsval2lem  15487  m1lgs  15562  1vgrex  15617  djucllem  15736  bdrabexg  15842  bdunexb  15856  peano5set  15876  speano5  15880  bj-omtrans  15892  pwf1oexmid  15936  nninfsellemeq  15951  iswomninnlem  15988