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  1360  mp3an12  1363  mp3an13  1364  ax9o  1746  sbnfc2  3188  ssdifss  3337  undifss  3575  uneqdifeqim  3580  elssuni  3921  csbexa  4218  difexg  4231  rabexg  4233  abssexg  4272  snexg  4274  copsexg  4336  sotritric  4421  sotritrieq  4422  trsuc  4519  oneli  4525  unexb  4539  opeluu  4547  rabxfr  4567  reuhyp  4569  ordunisuc2r  4612  reg3exmid  4678  brrelex12i  4768  brrelex1i  4769  brrelex2i  4770  xpss2  4837  opabid2  4861  eliunxp  4869  releldmi  4971  relelrni  4972  dmexg  4996  rnexg  4997  elres  5049  resexg  5053  relbrcnvg  5115  brcodir  5124  sotri  5132  sotri2  5134  sotri3  5135  dfrel2  5187  coi1  5252  fco  5500  fssres  5512  fabexg  5524  fvopab3g  5719  mptrcl  5729  mpteqb  5737  elfvmptrab1  5741  ffvelcdmi  5781  fsn2  5821  dfmptg  5827  fcof  5833  fvpr1  5858  fvconst2  5870  mptexg  5879  oprabid  6050  ovprc  6054  caovcl  6177  caovass  6183  caovdi  6202  elmpocl  6217  relmptopab  6224  ofexg  6240  resfunexgALT  6270  fo1stresm  6324  fo2ndresm  6325  1stexg  6330  2ndexg  6331  elopabi  6360  mpoexxg  6375  elmpom  6403  mpoxopn0yelv  6405  rntpos  6423  smores  6458  tfr0dm  6488  tfrlemibxssdm  6493  tfrexlem  6500  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  rdgruledefgg  6541  rdgruledefg  6542  rdgivallem  6547  rdgexg  6555  frec0g  6563  ordgt0ge1  6603  omfnex  6617  oeiv  6624  nna0r  6646  nnm0r  6647  nnsucsssuc  6660  nn2m  6695  nnaordex  6696  nnawordex  6697  ecdmn0m  6746  ecelqsi  6758  ecidg  6768  ectocl  6771  encv  6915  f1oen  6932  ssdomg  6952  map1  6987  fiprc  6990  dom1o  7002  xpdom1  7019  fict  7055  isinfinf  7086  ac6sfi  7087  xpfi  7124  en1eqsn  7147  fidcenumlemr  7154  fiss  7176  eqinfti  7219  djueq2  7240  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djuf1olem  7252  djulclb  7254  inl11  7264  eldju1st  7270  1stinl  7273  2ndinl  7274  1stinr  7275  2ndinr  7276  ctssdccl  7310  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  finacn  7419  djucomen  7431  exmidapne  7479  0nnq  7584  mulidnq  7609  archnqq  7637  prarloclemarch2  7639  nqnq0pi  7658  nq0m0r  7676  nq02m  7685  prarloclemlt  7713  prarloclemn  7719  prarloclem5  7720  addnqprllem  7747  addnqprulem  7748  appdivnq  7783  1idprl  7810  1idpru  7811  addextpr  7841  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemnbj  7887  caucvgprlemloc  7895  caucvgprprlemnbj  7913  caucvgprprlemloc  7923  caucvgprprlemaddq  7928  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemloc  7941  suplocexprlemlub  7944  0nsr  7969  ltsosr  7984  recexgt0sr  7993  prsrpos  8005  caucvgsr  8022  mappsrprg  8024  suplocsrlem  8028  mulresr  8058  axcnre  8101  axpre-ltwlin  8103  mullid  8177  0re  8179  axmulgt0  8251  ltnsym2  8270  eqlei  8273  ltnei  8283  muladd11  8312  cnegex  8357  0cnALT  8369  negcl  8379  negneg  8429  mul02  8566  mulm1  8579  lt0neg2  8649  le0neg2  8651  recexre  8758  recexgt0  8760  mulge0  8799  gt0ap0i  8807  recextlem1  8831  recexap  8833  recclapzi  8917  recap0apzi  8918  recidapzi  8919  divassapzi  8942  divmulapzi  8943  divdirapzi  8944  rerecclapzi  8956  ltp1  9024  recgt0i  9086  ltmul1i  9100  ltdiv1i  9101  ltmuldivi  9102  ltmul2i  9103  lemul1i  9104  lemul2i  9105  sup3exmid  9137  nngt1ne1  9178  nnrecre  9180  nn0ge0  9427  nn0addcl  9437  nn0mulcl  9438  zgt0ge1  9538  dfuzi  9590  eluzel2  9760  eluz2b1  9835  uz2m1nn  9839  elnn0dc  9845  elnndc  9846  nn01to3  9851  zq  9860  nnrecq  9879  rpge0  9901  rpreccl  9915  mnflt  10018  pnfnlt  10022  mnfle  10027  xrlelttr  10041  xrltletr  10042  xrletr  10043  xgepnf  10051  xlt0neg2  10074  xle0neg2  10076  xaddpnf2  10082  xaddmnf2  10084  xaddid2  10098  elioomnf  10203  ige3m2fz  10284  fzshftral  10343  ige2m1fz1  10344  1fv  10374  4fvwrd4  10375  rebtwn2zlemstep  10513  qbtwnxr  10518  btwnzge0  10561  zmodid2  10615  q2txmodxeq0  10647  frec2uzrand  10668  frecuzrdgtcl  10675  frecfzennn  10689  nn0ennn  10696  uzennn  10699  0exp  10837  sqgt0api  10888  subsq2  10910  qsqeqor  10913  bernneq  10923  faclbnd  11004  faclbnd2  11005  faclbnd3  11006  hashinfuni  11040  hashxp  11091  iswrdiz  11124  lsw0  11165  ccatlid  11187  s1leng  11205  s1fv  11207  s111  11212  pfx0g  11261  2shfti  11409  reim  11430  imcl  11432  crim  11436  caucvgre  11559  rennim  11580  resqrexlemdecn  11590  qabsor  11653  absimle  11662  sqrtthi  11697  sqrtcli  11698  sqrtgt0i  11699  sqrtmsqi  11700  sqrtsqi  11701  sqsqrti  11702  sqrtge0i  11703  absidi  11704  absnidi  11705  xrmaxiflemlub  11826  serclim0  11883  fsum2d  12014  fsumcnv  12016  fsumconst  12033  modfsummodlem1  12035  fsumabs  12044  binom11  12065  prodf1  12121  prodfclim1  12123  prodsnf  12171  fprod2d  12202  fprodcnv  12204  efzval  12262  eftlub  12269  efsep  12270  ef4p  12273  efgt1  12276  reef11  12278  sinf  12283  cosf  12284  efi4p  12296  sinneg  12305  cosneg  12306  efival  12311  efmival  12312  cos01gt0  12342  sin02gt0  12343  absefib  12350  efieq1re  12351  demoivre  12352  demoivreALT  12353  eirraplem  12356  0dvds  12390  odd2np1lem  12451  odd2np1  12452  even2n  12453  mod2eq0even  12457  2teven  12466  opoe  12474  omoe  12475  opeo  12476  omeo  12477  m1exp1  12480  bits0e  12528  bits0o  12529  bitsinv1  12541  gcd0id  12568  gcdid0  12569  1gcd  12581  lcmdvds  12669  isprm2lem  12706  isprm3  12708  prmgt1  12722  coprm  12734  isevengcd2  12748  isoddgcd1  12749  sqpweven  12765  2sqpwodd  12766  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem14  12868  pythagtriplem16  12870  pc2dvds  12921  oddprmdvds  12945  pockthi  12949  1arith2  12959  unennn  13036  ctinfomlemom  13066  qnnen  13070  ssnnctlemct  13085  strslfv  13145  strle1g  13207  1strbas  13218  tgval  13363  ismgmn0  13459  mulgval  13727  mulgfng  13729  mulg0  13730  mulg1  13734  mulg2  13736  isnsg  13807  ringidvalg  13993  issrg  13997  subrgpropd  14286  rrgval  14295  islmod  14324  scaffvalg  14339  islssm  14390  sraval  14470  mopnset  14585  metuex  14588  zrhval  14650  zrhvalg  14651  zrhex  14654  psrbag  14702  istopon  14756  eltg4i  14798  eltg3  14800  tg1  14802  tg2  14803  topnex  14829  cldrcl  14845  restsn  14923  lmrcl  14935  metflem  15092  xmetf  15093  ismet2  15097  xmeteq0  15102  xmettri2  15104  xmetpsmet  15112  xmetres2  15122  blfvalps  15128  blex  15130  blvalps  15131  blval  15132  blfps  15152  blf  15153  mopnval  15185  cnbl0  15277  cnblcld  15278  blssioo  15296  resubmet  15299  cncfmet  15335  cnplimcim  15410  cnlimcim  15414  cnlimc  15415  dvfgg  15431  dvfpm  15432  dvfcnpm  15433  dvcj  15452  dvmptfsum  15468  reeff1olem  15514  ef2kpi  15549  sinperlem  15551  sin2kpi  15554  cos2kpi  15555  sinhalfpip  15563  sinhalfpim  15564  coshalfpip  15565  coshalfpim  15566  sincosq1sgn  15569  sinq12gt0  15573  sinkpi  15590  reeflog  15606  relogef  15607  logrpap0b  15619  loggt0b  15634  1cxp  15643  ecxp  15644  2logb9irrap  15720  0sgm  15728  lgsval2lem  15758  m1lgs  15833  1vgrex  15890  upgrfi  15972  umgredgnlp  16022  wlkop  16218  clwwlkn0  16278  djucllem  16447  bdrabexg  16552  bdunexb  16566  peano5set  16586  speano5  16590  bj-omtrans  16602  pw1ninf  16641  pwf1oexmid  16651  nninfsellemeq  16667  iswomninnlem  16705