Theorem mpan 421

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mp2an  423  mpanl12  433  mp3an1  1303  mp3an12  1306  mp3an13  1307  ax9o  1677  sbnfc2  3065  ssdifss  3211  undifss  3448  uneqdifeqim  3453  elssuni  3772  csbexa  4065  difexg  4077  rabexg  4079  abssexg  4114  snexg  4116  copsexg  4174  sotritric  4254  sotritrieq  4255  trsuc  4352  oneli  4358  unexb  4371  opeluu  4379  rabxfr  4399  reuhyp  4401  ordunisuc2r  4438  reg3exmid  4502  brrelex12i  4589  brrelex1i  4590  brrelex2i  4591  xpss2  4658  opabid2  4678  eliunxp  4686  releldmi  4786  relelrni  4787  dmexg  4811  rnexg  4812  elres  4863  resexg  4867  relbrcnvg  4926  brcodir  4934  sotri  4942  sotri2  4944  sotri3  4945  dfrel2  4997  coi1  5062  fco  5296  fssres  5306  fabexg  5318  fvopab3g  5502  mptrcl  5511  mpteqb  5519  elfvmptrab1  5523  ffvelrni  5562  fsn2  5602  dfmptg  5607  fvpr1  5632  fvconst2  5644  mptexg  5653  oprabid  5811  ovprc  5814  caovcl  5933  caovass  5939  caovdi  5958  elmpocl  5976  ofexg  5994  resfunexgALT  6016  fo1stresm  6067  fo2ndresm  6068  1stexg  6073  2ndexg  6074  elopabi  6101  mpoexxg  6116  mpoxopn0yelv  6144  rntpos  6162  smores  6197  tfr0dm  6227  tfrlemibxssdm  6232  tfrexlem  6239  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  rdgruledefgg  6280  rdgruledefg  6281  rdgivallem  6286  rdgexg  6294  frec0g  6302  ordgt0ge1  6340  omfnex  6353  oeiv  6360  nna0r  6382  nnm0r  6383  nnsucsssuc  6396  nn2m  6430  nnaordex  6431  nnawordex  6432  ecdmn0m  6479  ecelqsi  6491  ecidg  6501  ectocl  6504  encv  6648  f1oen  6661  ssdomg  6680  map1  6714  fiprc  6717  xpdom1  6737  fict  6770  isinfinf  6799  ac6sfi  6800  xpfi  6826  en1eqsn  6844  fidcenumlemr  6851  fiss  6873  eqinfti  6915  djueq2  6934  djulclr  6942  djurclr  6943  djulcl  6944  djurcl  6945  djuf1olem  6946  djulclb  6948  inl11  6958  eldju1st  6964  1stinl  6967  2ndinl  6968  1stinr  6969  2ndinr  6970  ctssdccl  7004  isomnimap  7017  ismkvmap  7036  iswomnimap  7048  djucomen  7089  0nnq  7196  mulidnq  7221  archnqq  7249  prarloclemarch2  7251  nqnq0pi  7270  nq0m0r  7288  nq02m  7297  prarloclemlt  7325  prarloclemn  7331  prarloclem5  7332  addnqprllem  7359  addnqprulem  7360  appdivnq  7395  1idprl  7422  1idpru  7423  addextpr  7453  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemnbj  7499  caucvgprlemloc  7507  caucvgprprlemnbj  7525  caucvgprprlemloc  7535  caucvgprprlemaddq  7540  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemloc  7553  suplocexprlemlub  7556  0nsr  7581  ltsosr  7596  recexgt0sr  7605  prsrpos  7617  caucvgsr  7634  mappsrprg  7636  suplocsrlem  7640  mulresr  7670  axcnre  7713  axpre-ltwlin  7715  mulid2  7788  0re  7790  axmulgt0  7860  ltnsym2  7878  eqlei  7881  ltnei  7891  muladd11  7919  cnegex  7964  0cnALT  7976  negcl  7986  negneg  8036  mul02  8173  mulm1  8186  lt0neg2  8255  le0neg2  8257  recexre  8364  recexgt0  8366  mulge0  8405  gt0ap0i  8413  recextlem1  8436  recexap  8438  recclapzi  8521  recap0apzi  8522  recidapzi  8523  divassapzi  8546  divmulapzi  8547  divdirapzi  8548  rerecclapzi  8560  ltp1  8626  recgt0i  8688  ltmul1i  8702  ltdiv1i  8703  ltmuldivi  8704  ltmul2i  8705  lemul1i  8706  lemul2i  8707  sup3exmid  8739  nngt1ne1  8779  nnrecre  8781  nn0ge0  9026  nn0addcl  9036  nn0mulcl  9037  zgt0ge1  9136  dfuzi  9185  eluzel2  9355  eluz2b1  9422  uz2m1nn  9426  nn01to3  9436  zq  9445  nnrecq  9464  rpge0  9483  rpreccl  9497  mnflt  9599  pnfnlt  9603  mnfle  9608  xrlelttr  9619  xrltletr  9620  xrletr  9621  xgepnf  9629  xlt0neg2  9652  xle0neg2  9654  xaddpnf2  9660  xaddmnf2  9662  xaddid2  9676  elioomnf  9781  ige3m2fz  9860  fzshftral  9919  ige2m1fz1  9920  1fv  9947  4fvwrd4  9948  rebtwn2zlemstep  10061  qbtwnxr  10066  btwnzge0  10104  zmodid2  10156  q2txmodxeq0  10188  frec2uzrand  10209  frecuzrdgtcl  10216  frecfzennn  10230  nn0ennn  10237  uzennn  10240  0exp  10359  sqgt0api  10409  subsq2  10431  bernneq  10443  faclbnd  10519  faclbnd2  10520  faclbnd3  10521  hashinfuni  10555  hashxp  10604  2shfti  10635  reim  10656  imcl  10658  crim  10662  caucvgre  10785  rennim  10806  resqrexlemdecn  10816  qabsor  10879  absimle  10888  sqrtthi  10923  sqrtcli  10924  sqrtgt0i  10925  sqrtmsqi  10926  sqrtsqi  10927  sqsqrti  10928  sqrtge0i  10929  absidi  10930  absnidi  10931  xrmaxiflemlub  11049  serclim0  11106  fsum2d  11236  fsumcnv  11238  fsumconst  11255  modfsummodlem1  11257  fsumabs  11266  binom11  11287  prodf1  11343  prodfclim1  11345  efzval  11426  eftlub  11433  efsep  11434  ef4p  11437  efgt1  11440  reef11  11442  sinf  11447  cosf  11448  efi4p  11460  sinneg  11469  cosneg  11470  efival  11475  efmival  11476  cos01gt0  11505  sin02gt0  11506  absefib  11513  efieq1re  11514  demoivre  11515  demoivreALT  11516  eirraplem  11519  0dvds  11549  odd2np1lem  11605  odd2np1  11606  even2n  11607  mod2eq0even  11611  2teven  11620  opoe  11628  omoe  11629  opeo  11630  omeo  11631  m1exp1  11634  gcd0id  11703  gcdid0  11704  1gcd  11716  lcmdvds  11796  isprm2lem  11833  isprm3  11835  prmgt1  11848  coprm  11858  isevengcd2  11872  isoddgcd1  11873  sqpweven  11889  2sqpwodd  11890  unennn  11946  ctinfomlemom  11976  qnnen  11980  strslfv  12042  strle1g  12088  1strbas  12097  istopon  12219  tgval  12257  eltg4i  12263  eltg3  12265  tg1  12267  tg2  12268  topnex  12294  cldrcl  12310  restsn  12388  lmrcl  12399  metflem  12557  xmetf  12558  ismet2  12562  xmeteq0  12567  xmettri2  12569  xmetpsmet  12577  xmetres2  12587  blfvalps  12593  blex  12595  blvalps  12596  blval  12597  blfps  12617  blf  12618  mopnval  12650  cnbl0  12742  cnblcld  12743  blssioo  12753  resubmet  12756  cncfmet  12787  cnplimcim  12844  cnlimcim  12848  cnlimc  12849  dvfgg  12865  dvfpm  12866  dvfcnpm  12867  dvcj  12881  reeff1olem  12900  ef2kpi  12935  sinperlem  12937  sin2kpi  12940  cos2kpi  12941  sinhalfpip  12949  sinhalfpim  12950  coshalfpip  12951  coshalfpim  12952  sincosq1sgn  12955  sinq12gt0  12959  sinkpi  12976  reeflog  12992  relogef  12993  logrpap0b  13005  loggt0b  13020  1cxp  13029  ecxp  13030  2logb9irrap  13102  djucllem  13178  bdrabexg  13275  bdunexb  13289  peano5set  13309  speano5  13313  bj-omtrans  13325  pwf1oexmid  13367  nninfsellemeq  13385  iswomninnlem  13417