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  5826  fcof  5832  fvpr1  5857  fvconst2  5869  mptexg  5878  oprabid  6049  ovprc  6053  caovcl  6176  caovass  6182  caovdi  6201  elmpocl  6216  relmptopab  6223  ofexg  6239  resfunexgALT  6269  fo1stresm  6323  fo2ndresm  6324  1stexg  6329  2ndexg  6330  elopabi  6359  mpoexxg  6374  elmpom  6402  mpoxopn0yelv  6404  rntpos  6422  smores  6457  tfr0dm  6487  tfrlemibxssdm  6492  tfrexlem  6499  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  rdgruledefgg  6540  rdgruledefg  6541  rdgivallem  6546  rdgexg  6554  frec0g  6562  ordgt0ge1  6602  omfnex  6616  oeiv  6623  nna0r  6645  nnm0r  6646  nnsucsssuc  6659  nn2m  6694  nnaordex  6695  nnawordex  6696  ecdmn0m  6745  ecelqsi  6757  ecidg  6767  ectocl  6770  encv  6914  f1oen  6931  ssdomg  6951  map1  6986  fiprc  6989  dom1o  7001  xpdom1  7018  fict  7054  isinfinf  7085  ac6sfi  7086  xpfi  7123  en1eqsn  7146  fidcenumlemr  7153  fiss  7175  eqinfti  7218  djueq2  7239  djulclr  7247  djurclr  7248  djulcl  7249  djurcl  7250  djuf1olem  7251  djulclb  7253  inl11  7263  eldju1st  7269  1stinl  7272  2ndinl  7273  1stinr  7274  2ndinr  7275  ctssdccl  7309  isomnimap  7335  ismkvmap  7352  iswomnimap  7364  finacn  7418  djucomen  7430  exmidapne  7478  0nnq  7583  mulidnq  7608  archnqq  7636  prarloclemarch2  7638  nqnq0pi  7657  nq0m0r  7675  nq02m  7684  prarloclemlt  7712  prarloclemn  7718  prarloclem5  7719  addnqprllem  7746  addnqprulem  7747  appdivnq  7782  1idprl  7809  1idpru  7810  addextpr  7840  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemnbj  7886  caucvgprlemloc  7894  caucvgprprlemnbj  7912  caucvgprprlemloc  7922  caucvgprprlemaddq  7927  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemloc  7940  suplocexprlemlub  7943  0nsr  7968  ltsosr  7983  recexgt0sr  7992  prsrpos  8004  caucvgsr  8021  mappsrprg  8023  suplocsrlem  8027  mulresr  8057  axcnre  8100  axpre-ltwlin  8102  mullid  8176  0re  8178  axmulgt0  8250  ltnsym2  8269  eqlei  8272  ltnei  8282  muladd11  8311  cnegex  8356  0cnALT  8368  negcl  8378  negneg  8428  mul02  8565  mulm1  8578  lt0neg2  8648  le0neg2  8650  recexre  8757  recexgt0  8759  mulge0  8798  gt0ap0i  8806  recextlem1  8830  recexap  8832  recclapzi  8916  recap0apzi  8917  recidapzi  8918  divassapzi  8941  divmulapzi  8942  divdirapzi  8943  rerecclapzi  8955  ltp1  9023  recgt0i  9085  ltmul1i  9099  ltdiv1i  9100  ltmuldivi  9101  ltmul2i  9102  lemul1i  9103  lemul2i  9104  sup3exmid  9136  nngt1ne1  9177  nnrecre  9179  nn0ge0  9426  nn0addcl  9436  nn0mulcl  9437  zgt0ge1  9537  dfuzi  9589  eluzel2  9759  eluz2b1  9834  uz2m1nn  9838  elnn0dc  9844  elnndc  9845  nn01to3  9850  zq  9859  nnrecq  9878  rpge0  9900  rpreccl  9914  mnflt  10017  pnfnlt  10021  mnfle  10026  xrlelttr  10040  xrltletr  10041  xrletr  10042  xgepnf  10050  xlt0neg2  10073  xle0neg2  10075  xaddpnf2  10081  xaddmnf2  10083  xaddid2  10097  elioomnf  10202  ige3m2fz  10283  fzshftral  10342  ige2m1fz1  10343  1fv  10373  4fvwrd4  10374  rebtwn2zlemstep  10511  qbtwnxr  10516  btwnzge0  10559  zmodid2  10613  q2txmodxeq0  10645  frec2uzrand  10666  frecuzrdgtcl  10673  frecfzennn  10687  nn0ennn  10694  uzennn  10697  0exp  10835  sqgt0api  10886  subsq2  10908  qsqeqor  10911  bernneq  10921  faclbnd  11002  faclbnd2  11003  faclbnd3  11004  hashinfuni  11038  hashxp  11089  iswrdiz  11119  lsw0  11160  ccatlid  11182  s1leng  11200  s1fv  11202  s111  11207  pfx0g  11256  2shfti  11391  reim  11412  imcl  11414  crim  11418  caucvgre  11541  rennim  11562  resqrexlemdecn  11572  qabsor  11635  absimle  11644  sqrtthi  11679  sqrtcli  11680  sqrtgt0i  11681  sqrtmsqi  11682  sqrtsqi  11683  sqsqrti  11684  sqrtge0i  11685  absidi  11686  absnidi  11687  xrmaxiflemlub  11808  serclim0  11865  fsum2d  11995  fsumcnv  11997  fsumconst  12014  modfsummodlem1  12016  fsumabs  12025  binom11  12046  prodf1  12102  prodfclim1  12104  prodsnf  12152  fprod2d  12183  fprodcnv  12185  efzval  12243  eftlub  12250  efsep  12251  ef4p  12254  efgt1  12257  reef11  12259  sinf  12264  cosf  12265  efi4p  12277  sinneg  12286  cosneg  12287  efival  12292  efmival  12293  cos01gt0  12323  sin02gt0  12324  absefib  12331  efieq1re  12332  demoivre  12333  demoivreALT  12334  eirraplem  12337  0dvds  12371  odd2np1lem  12432  odd2np1  12433  even2n  12434  mod2eq0even  12438  2teven  12447  opoe  12455  omoe  12456  opeo  12457  omeo  12458  m1exp1  12461  bits0e  12509  bits0o  12510  bitsinv1  12522  gcd0id  12549  gcdid0  12550  1gcd  12562  lcmdvds  12650  isprm2lem  12687  isprm3  12689  prmgt1  12703  coprm  12715  isevengcd2  12729  isoddgcd1  12730  sqpweven  12746  2sqpwodd  12747  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem14  12849  pythagtriplem16  12851  pc2dvds  12902  oddprmdvds  12926  pockthi  12930  1arith2  12940  unennn  13017  ctinfomlemom  13047  qnnen  13051  ssnnctlemct  13066  strslfv  13126  strle1g  13188  1strbas  13199  tgval  13344  ismgmn0  13440  mulgval  13708  mulgfng  13710  mulg0  13711  mulg1  13715  mulg2  13717  isnsg  13788  ringidvalg  13973  issrg  13977  subrgpropd  14266  rrgval  14275  islmod  14304  scaffvalg  14319  islssm  14370  sraval  14450  mopnset  14565  metuex  14568  zrhval  14630  zrhvalg  14631  zrhex  14634  psrbag  14682  istopon  14736  eltg4i  14778  eltg3  14780  tg1  14782  tg2  14783  topnex  14809  cldrcl  14825  restsn  14903  lmrcl  14915  metflem  15072  xmetf  15073  ismet2  15077  xmeteq0  15082  xmettri2  15084  xmetpsmet  15092  xmetres2  15102  blfvalps  15108  blex  15110  blvalps  15111  blval  15112  blfps  15132  blf  15133  mopnval  15165  cnbl0  15257  cnblcld  15258  blssioo  15276  resubmet  15279  cncfmet  15315  cnplimcim  15390  cnlimcim  15394  cnlimc  15395  dvfgg  15411  dvfpm  15412  dvfcnpm  15413  dvcj  15432  dvmptfsum  15448  reeff1olem  15494  ef2kpi  15529  sinperlem  15531  sin2kpi  15534  cos2kpi  15535  sinhalfpip  15543  sinhalfpim  15544  coshalfpip  15545  coshalfpim  15546  sincosq1sgn  15549  sinq12gt0  15553  sinkpi  15570  reeflog  15586  relogef  15587  logrpap0b  15599  loggt0b  15614  1cxp  15623  ecxp  15624  2logb9irrap  15700  0sgm  15708  lgsval2lem  15738  m1lgs  15813  1vgrex  15870  upgrfi  15952  umgredgnlp  16002  wlkop  16198  clwwlkn0  16258  djucllem  16396  bdrabexg  16501  bdunexb  16515  peano5set  16535  speano5  16539  bj-omtrans  16551  pw1ninf  16590  pwf1oexmid  16600  nninfsellemeq  16616  iswomninnlem  16653