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  1361  mp3an12  1364  mp3an13  1365  ax9o  1746  sbnfc2  3202  ssdifss  3353  undifss  3594  uneqdifeqim  3599  elssuni  3947  csbexa  4244  difexg  4257  rabexg  4260  abssexg  4300  snexg  4302  copsexg  4365  sotritric  4450  sotritrieq  4451  trsuc  4548  oneli  4554  unexb  4568  opeluu  4576  rabxfr  4596  reuhyp  4598  ordunisuc2r  4641  reg3exmid  4707  brrelex12i  4797  brrelex1i  4798  brrelex2i  4799  xpss2  4866  opabid2  4891  eliunxp  4899  releldmi  5001  relelrni  5002  dmexg  5026  rnexg  5027  elres  5079  resexg  5083  relbrcnvg  5146  brcodir  5155  sotri  5163  sotri2  5165  sotri3  5166  dfrel2  5218  coi1  5283  fco  5532  fssres  5545  fabexg  5559  fvopab3g  5755  mptrcl  5765  mpteqb  5773  elfvmptrab1  5777  ffvelcdmi  5816  fsn2  5856  dfmptg  5862  fcof  5868  fvpr1  5893  fvconst2  5905  mptexg  5916  oprabid  6090  ovprc  6094  caovcl  6217  caovass  6223  caovdi  6242  elmpocl  6257  relmptopab  6264  ofexg  6280  resfunexgALT  6310  fo1stresm  6368  fo2ndresm  6369  1stexg  6374  2ndexg  6375  elopabi  6404  mpoexxg  6419  elmpom  6447  supp0  6451  mpoxopn0yelv  6483  rntpos  6501  smores  6536  tfr0dm  6566  tfrlemibxssdm  6571  tfrexlem  6578  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  rdgruledefgg  6619  rdgruledefg  6620  rdgivallem  6625  rdgexg  6633  frec0g  6641  ordgt0ge1  6681  omfnex  6695  oeiv  6702  nna0r  6724  nnm0r  6725  nnsucsssuc  6738  nn2m  6773  nnaordex  6774  nnawordex  6775  ecdmn0m  6824  ecelqsi  6836  ecidg  6846  ectocl  6849  encv  6994  f1oen  7011  ssdomg  7031  map1  7067  fiprc  7070  dom1o  7082  xpdom1  7099  fict  7136  isinfinf  7167  ac6sfi  7168  xpfi  7205  en1eqsn  7231  fidcenumlemr  7238  fiss  7277  fipwfi  7285  eqinfti  7324  djueq2  7345  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djuf1olem  7357  djulclb  7359  inl11  7369  eldju1st  7375  1stinl  7378  2ndinl  7379  1stinr  7380  2ndinr  7381  ctssdccl  7415  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  finacn  7524  djucomen  7536  exmidapne  7590  0nnq  7695  mulidnq  7720  archnqq  7748  prarloclemarch2  7750  nqnq0pi  7769  nq0m0r  7787  nq02m  7796  prarloclemlt  7824  prarloclemn  7830  prarloclem5  7831  addnqprllem  7858  addnqprulem  7859  appdivnq  7894  1idprl  7921  1idpru  7922  addextpr  7952  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemnbj  7998  caucvgprlemloc  8006  caucvgprprlemnbj  8024  caucvgprprlemloc  8034  caucvgprprlemaddq  8039  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemloc  8052  suplocexprlemlub  8055  0nsr  8080  ltsosr  8095  recexgt0sr  8104  prsrpos  8116  caucvgsr  8133  mappsrprg  8135  suplocsrlem  8139  mulresr  8169  axcnre  8212  axpre-ltwlin  8214  mullid  8288  0re  8290  axmulgt0  8361  ltnsym2  8380  eqlei  8383  ltnei  8393  muladd11  8422  cnegex  8467  0cnALT  8479  negcl  8489  negneg  8539  mul02  8677  mulm1  8690  lt0neg2  8760  le0neg2  8762  recexre  8869  recexgt0  8871  mulge0  8910  gt0ap0i  8918  recextlem1  8942  recexap  8944  recclapzi  9028  recap0apzi  9029  recidapzi  9030  divassapzi  9053  divmulapzi  9054  divdirapzi  9055  rerecclapzi  9067  ltp1  9135  recgt0i  9197  ltmul1i  9211  ltdiv1i  9212  ltmuldivi  9213  ltmul2i  9214  lemul1i  9215  lemul2i  9216  sup3exmid  9248  nngt1ne1  9289  nnrecre  9291  nn0ge0  9538  nn0addcl  9548  nn0mulcl  9549  zgt0ge1  9653  dfuzi  9706  eluzel2  9876  eluz2b1  9951  uz2m1nn  9955  elnn0dc  9961  elnndc  9962  nn01to3  9967  zq  9976  nnrecq  9995  rpge0  10017  rpreccl  10031  mnflt  10135  pnfnlt  10139  mnfle  10144  xrlelttr  10158  xrltletr  10159  xrletr  10160  xgepnf  10168  xlt0neg2  10191  xle0neg2  10193  xaddpnf2  10199  xaddmnf2  10201  xaddid2  10215  elioomnf  10320  ige3m2fz  10403  fzshftral  10464  ige2m1fz1  10465  1fv  10495  4fvwrd4  10496  rebtwn2zlemstep  10636  qbtwnxr  10641  btwnzge0  10684  zmodid2  10738  q2txmodxeq0  10770  frec2uzrand  10791  frecuzrdgtcl  10798  frecfzennn  10812  nn0ennn  10819  uzennn  10822  0exp  10960  sqgt0api  11011  subsq2  11033  qsqeqor  11036  bernneq  11047  faclbnd  11128  faclbnd2  11129  faclbnd3  11130  hashinfuni  11165  hashxp  11216  hashpwfi  11218  iswrdiz  11256  lsw0  11297  ccatlid  11319  s1leng  11337  s1fv  11339  s111  11344  pfx0g  11393  2shfti  11541  reim  11562  imcl  11564  crim  11568  caucvgre  11691  rennim  11712  resqrexlemdecn  11722  qabsor  11785  absimle  11794  sqrtthi  11829  sqrtcli  11830  sqrtgt0i  11831  sqrtmsqi  11832  sqrtsqi  11833  sqsqrti  11834  sqrtge0i  11835  absidi  11836  absnidi  11837  xrmaxiflemlub  11958  serclim0  12015  fsum2d  12146  fsumcnv  12148  fsumconst  12165  modfsummodlem1  12167  fsumabs  12176  binom11  12197  prodf1  12253  prodfclim1  12255  prodsnf  12303  fprod2d  12334  fprodcnv  12336  efzval  12394  eftlub  12401  efsep  12402  ef4p  12405  efgt1  12408  reef11  12410  sinf  12415  cosf  12416  efi4p  12428  sinneg  12437  cosneg  12438  efival  12443  efmival  12444  cos01gt0  12474  sin02gt0  12475  absefib  12482  efieq1re  12483  demoivre  12484  demoivreALT  12485  eirraplem  12488  0dvds  12522  odd2np1lem  12583  odd2np1  12584  even2n  12585  mod2eq0even  12589  2teven  12598  opoe  12606  omoe  12607  opeo  12608  omeo  12609  m1exp1  12612  bits0e  12660  bits0o  12661  bitsinv1  12673  gcd0id  12700  gcdid0  12701  1gcd  12713  lcmdvds  12801  isprm2lem  12838  isprm3  12840  prmgt1  12854  coprm  12866  isevengcd2  12880  isoddgcd1  12881  sqpweven  12897  2sqpwodd  12898  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem14  13000  pythagtriplem16  13002  pc2dvds  13053  oddprmdvds  13077  pockthi  13081  1arith2  13091  unennn  13232  ctinfomlemom  13262  qnnen  13266  ssnnctlemct  13281  strslfv  13341  strle1g  13403  1strbas  13414  tgval  13559  ismgmn0  13621  mulgval  13875  mulgfng  13877  mulg0  13878  mulg1  13882  mulg2  13884  isnsg  13955  ringidvalg  14204  issrg  14208  subrgpropd  14499  rrgval  14508  islmod  14565  scaffvalg  14580  islssm  14631  sraval  14711  mopnset  14826  metuex  14829  zrhval  14891  zrhvalg  14892  zrhex  14895  psrbag  14943  psrbagaddclfi  14951  istopon  15004  eltg4i  15046  eltg3  15048  tg1  15050  tg2  15051  topnex  15077  cldrcl  15093  restsn  15171  lmrcl  15183  metflem  15340  xmetf  15341  ismet2  15345  xmeteq0  15350  xmettri2  15352  xmetpsmet  15360  xmetres2  15370  blfvalps  15376  blex  15378  blvalps  15379  blval  15380  blfps  15400  blf  15401  mopnval  15433  cnbl0  15525  cnblcld  15526  blssioo  15544  resubmet  15547  cncfmet  15583  cnplimcim  15658  cnlimcim  15662  cnlimc  15663  dvfgg  15679  dvfpm  15680  dvfcnpm  15681  dvcj  15700  dvmptfsum  15716  reeff1olem  15762  ef2kpi  15797  sinperlem  15799  sin2kpi  15802  cos2kpi  15803  sinhalfpip  15811  sinhalfpim  15812  coshalfpip  15813  coshalfpim  15814  sincosq1sgn  15817  sinq12gt0  15821  sinkpi  15838  reeflog  15854  relogef  15855  logrpap0b  15867  loggt0b  15882  1cxp  15891  ecxp  15892  2logb9irrap  15968  0sgm  15979  lgsval2lem  16009  m1lgs  16084  1vgrex  16141  upgrfi  16223  umgredgnlp  16273  wlkop  16469  clwwlkn0  16529  djucllem  16698  bdrabexg  16802  bdunexb  16816  peano5set  16836  speano5  16840  bj-omtrans  16852  pw1ninf  16891  pwf1oexmid  16899  nninfsellemeq  16918  iswomninnlem  16960