Theorem mpan 428

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mp2an  430  mpanl12  440  mp3an1  1365  mp3an12  1368  mp3an13  1369  ax9o  1750  sbnfc2  3208  ssdifss  3359  undifss  3608  uneqdifeqim  3613  elssuni  3963  csbexa  4264  difexg  4277  rabexg  4281  abssexg  4321  snexg  4323  copsexg  4386  sotritric  4471  sotritrieq  4472  trsuc  4569  oneli  4575  unexb  4590  opeluu  4598  rabxfr  4618  reuhyp  4620  ordunisuc2r  4663  reg3exmid  4729  brrelex12i  4819  brrelex1i  4820  brrelex2i  4821  xpss2  4888  opabid2  4913  eliunxp  4921  releldmi  5023  relelrni  5024  dmexg  5048  rnexg  5049  elres  5101  resexg  5105  relbrcnvg  5169  brcodir  5178  sotri  5186  sotri2  5188  sotri3  5189  dfrel2  5241  coi1  5306  fco  5555  fssres  5568  fabexg  5582  fvopab3g  5781  mptrcl  5791  mpteqb  5799  elfvmptrab1  5804  fvopab4ndm  5806  ffvelcdmi  5845  fsn2  5885  dfmptg  5891  fcof  5897  fvpr1  5922  fvconst2  5934  mptexg  5945  oprabid  6120  ovprc  6124  caovcl  6247  caovass  6253  caovdi  6272  elmpocl  6287  relmptopab  6294  ofexg  6310  resfunexgALT  6341  fo1stresm  6399  fo2ndresm  6400  1stexg  6405  2ndexg  6406  elopabi  6435  mpoexxg  6450  elmpom  6478  supp0  6482  mpoxopn0yelv  6514  rntpos  6532  smores  6567  tfr0dm  6597  tfrlemibxssdm  6602  tfrexlem  6609  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  rdgruledefgg  6650  rdgruledefg  6651  rdgivallem  6656  rdgexg  6664  frec0g  6672  ordgt0ge1  6712  omfnex  6726  oeiv  6733  nna0r  6755  nnm0r  6756  nnsucsssuc  6769  nn2m  6804  nnaordex  6805  nnawordex  6806  ecdmn0m  6855  ecelqsi  6867  ecidg  6877  ectocl  6880  mapfset  6949  encv  7032  f1oen  7049  ssdomg  7069  map1  7105  fiprc  7108  dom1o  7120  xpdom1  7137  fict  7174  isinfinf  7205  ac6sfi  7206  xpfi  7243  en1eqsn  7270  fidcenumlemr  7277  fiss  7316  fipwfi  7327  eqinfti  7366  djueq2  7387  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  djuf1olem  7399  djulclb  7401  inl11  7411  eldju1st  7417  1stinl  7420  2ndinl  7421  1stinr  7422  2ndinr  7423  ctssdccl  7457  isomnimap  7483  ismkvmap  7500  iswomnimap  7512  finacn  7566  djucomen  7578  exmidapne  7632  0nnq  7737  mulidnq  7762  archnqq  7790  prarloclemarch2  7792  nqnq0pi  7811  nq0m0r  7829  nq02m  7838  prarloclemlt  7866  prarloclemn  7872  prarloclem5  7873  addnqprllem  7900  addnqprulem  7901  appdivnq  7936  1idprl  7963  1idpru  7964  addextpr  7994  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemnbj  8040  caucvgprlemloc  8048  caucvgprprlemnbj  8066  caucvgprprlemloc  8076  caucvgprprlemaddq  8081  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemloc  8094  suplocexprlemlub  8097  0nsr  8122  ltsosr  8137  recexgt0sr  8146  prsrpos  8158  caucvgsr  8175  mappsrprg  8177  suplocsrlem  8181  mulresr  8211  axcnre  8254  axpre-ltwlin  8256  mullid  8330  0re  8332  axmulgt0  8403  ltnsym2  8422  eqlei  8426  ltnei  8436  muladd11  8466  cnegex  8511  0cnALT  8523  negcl  8533  negneg  8583  mul02  8721  mulm1  8734  lt0neg2  8804  le0neg2  8806  recexre  8914  recexgt0  8916  mulge0  8955  gt0ap0i  8963  recextlem1  8987  recexap  8989  recclapzi  9075  recap0apzi  9076  recidapzi  9077  divassapzi  9100  divmulapzi  9101  divdirapzi  9102  rerecclapzi  9114  ltp1  9182  recgt0i  9244  ltmul1i  9258  ltdiv1i  9259  ltmuldivi  9260  ltmul2i  9261  lemul1i  9262  lemul2i  9263  sup3exmid  9295  nngt1ne1  9348  nnrecre  9350  nn0ge0  9599  nn0addcl  9609  nn0mulcl  9610  zgt0ge1  9714  dfuzi  9767  eluzel2  9942  eluz2b1  10017  uz2m1nn  10021  elnn0dc  10027  elnndc  10028  nn01to3  10033  zq  10042  nnrecq  10061  rpge0  10084  rpreccl  10098  mnflt  10202  pnfnlt  10206  mnfle  10211  xrlelttr  10225  xrltletr  10226  xrletr  10227  xgepnf  10235  xlt0neg2  10258  xle0neg2  10260  xaddpnf2  10266  xaddmnf2  10268  xaddid2  10282  elioomnf  10387  ige3m2fz  10471  fzshftral  10532  ige2m1fz1  10533  1fv  10563  4fvwrd4  10564  rebtwn2zlemstep  10704  qbtwnxr  10709  btwnzge0  10756  zmodid2  10810  q2txmodxeq0  10842  frec2uzrand  10863  frecuzrdgtcl  10870  frecfzennn  10884  nn0ennn  10891  uzennn  10894  0exp  11032  sqgt0api  11083  subsq2  11105  qsqeqor  11108  bernneq  11119  faclbnd  11201  faclbnd2  11202  faclbnd3  11203  hashinfuni  11238  hashxp  11289  hashpwfi  11291  iswrdiz  11333  lsw0  11374  ccatlid  11396  s1leng  11414  s1fv  11416  s111  11421  pfx0g  11470  2shfti  11618  reim  11639  imcl  11641  crim  11645  caucvgre  11769  rennim  11790  resqrexlemdecn  11800  qabsor  11863  absimle  11873  sqrtthi  11908  sqrtcli  11909  sqrtgt0i  11910  sqrtmsqi  11911  sqrtsqi  11912  sqsqrti  11913  sqrtge0i  11914  absidi  11915  absnidi  11916  xrmaxiflemlub  12039  serclim0  12096  fsum2d  12227  fsumcnv  12229  fsumconst  12246  modfsummodlem1  12248  fsumabs  12257  binom11  12278  prodf1  12334  prodfclim1  12336  prodsnf  12384  fprod2d  12415  fprodcnv  12417  efzval  12475  eftlub  12482  efsep  12483  ef4p  12486  efgt1  12489  reef11  12491  sinf  12496  cosf  12497  efi4p  12509  sinneg  12518  cosneg  12519  efival  12524  efmival  12525  cos01gt0  12555  sin02gt0  12556  absefib  12563  efieq1re  12564  demoivre  12565  demoivreALT  12566  eirraplem  12569  0dvds  12603  odd2np1lem  12664  odd2np1  12665  even2n  12666  mod2eq0even  12670  2teven  12679  opoe  12687  omoe  12688  opeo  12689  omeo  12690  m1exp1  12693  bits0e  12741  bits0o  12742  bitsinv1  12754  gcd0id  12781  gcdid0  12782  1gcd  12794  lcmdvds  12882  isprm2lem  12919  isprm3  12921  prmgt1  12936  coprm  12948  isevengcd2  12962  isoddgcd1  12963  sqpweven  12980  2sqpwodd  12981  sqrtrirr  13014  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem14  13085  pythagtriplem16  13087  pc2dvds  13138  oddprmdvds  13162  pockthi  13166  1arith2  13176  prmlem1a  13250  unennn  13346  ctinfomlemom  13376  qnnen  13380  ssnnctlemct  13395  strslfv  13455  slotm  13473  strle1g  13519  1strbas  13530  tgval  13675  ismgmn0  13737  mulgval  13984  mulgfng  13986  mulg0  13987  mulg1  13991  mulg2  13993  isnsg  14064  cntrval  14151  mgpplusg  14329  mgpbas  14332  ringidvalg  14371  ringidval  14372  issrg  14376  subrgpropd  14670  rrgval  14679  islmod  14736  scaffvalg  14752  islssm  14803  sraval  14883  mopnset  14998  metuex  15001  zrhval  15061  zrhvalg  15062  zrhex  15065  asclfval  15130  psrbag  15162  psrbagaddclfi  15170  istopon  15239  eltg4i  15281  eltg3  15283  tg1  15285  tg2  15286  topnex  15312  cldrcl  15328  restsn  15406  lmrcl  15418  metflem  15575  xmetf  15576  ismet2  15580  xmeteq0  15585  xmettri2  15587  xmetpsmet  15595  xmetres2  15605  blfvalps  15611  blex  15613  blvalps  15614  blval  15615  blfps  15635  blf  15636  mopnval  15668  cnbl0  15760  cnblcld  15761  blssioo  15779  resubmet  15782  cncfmet  15818  cnplimcim  15893  cnlimcim  15897  cnlimc  15898  dvfgg  15914  dvfpm  15915  dvfcnpm  15916  dvcj  15935  dvmptfsum  15951  reeff1olem  15997  ef2kpi  16033  sinperlem  16035  sin2kpi  16038  cos2kpi  16039  sinhalfpip  16047  sinhalfpim  16048  coshalfpip  16049  coshalfpim  16050  sincosq1sgn  16053  sinq12gt0  16057  sinkpi  16074  sineq0re  16076  reeflog  16092  relogef  16093  logrpap0b  16106  loggt0b  16121  1cxp  16133  ecxp  16134  2logb9irrap  16213  log2tlbndlog2  16220  log2ublem2  16222  0sgm  16254  chtublem  16295  pcbcctr  16303  bcp1ctr  16306  bclbnd  16307  bposlem1  16311  lgsval2lem  16334  m1lgs  16409  1vgrex  16466  upgrfi  16548  umgredgnlp  16598  wlkop  16794  clwwlkn0  16854  djucllem  17033  bdrabexg  17137  bdunexb  17151  peano5set  17171  speano5  17175  bj-omtrans  17187  pw1ninf  17226  pwf1oexmid  17234  nninfsellemeq  17263  iswomninnlem  17306