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 )

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  430  mpanl12  440  mp3an1  1365  mp3an12  1368  mp3an13  1369  ax9o  1750  sbnfc2  3208  ssdifss  3359  undifss  3605  uneqdifeqim  3610  elssuni  3958  csbexa  4257  difexg  4270  rabexg  4274  abssexg  4314  snexg  4316  copsexg  4379  sotritric  4464  sotritrieq  4465  trsuc  4562  oneli  4568  unexb  4583  opeluu  4591  rabxfr  4611  reuhyp  4613  ordunisuc2r  4656  reg3exmid  4722  brrelex12i  4812  brrelex1i  4813  brrelex2i  4814  xpss2  4881  opabid2  4906  eliunxp  4914  releldmi  5016  relelrni  5017  dmexg  5041  rnexg  5042  elres  5094  resexg  5098  relbrcnvg  5161  brcodir  5170  sotri  5178  sotri2  5180  sotri3  5181  dfrel2  5233  coi1  5298  fco  5547  fssres  5560  fabexg  5574  fvopab3g  5772  mptrcl  5782  mpteqb  5790  elfvmptrab1  5794  ffvelcdmi  5833  fsn2  5873  dfmptg  5879  fcof  5885  fvpr1  5910  fvconst2  5922  mptexg  5933  oprabid  6107  ovprc  6111  caovcl  6234  caovass  6240  caovdi  6259  elmpocl  6274  relmptopab  6281  ofexg  6297  resfunexgALT  6327  fo1stresm  6385  fo2ndresm  6386  1stexg  6391  2ndexg  6392  elopabi  6421  mpoexxg  6436  elmpom  6464  supp0  6468  mpoxopn0yelv  6500  rntpos  6518  smores  6553  tfr0dm  6583  tfrlemibxssdm  6588  tfrexlem  6595  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  rdgruledefgg  6636  rdgruledefg  6637  rdgivallem  6642  rdgexg  6650  frec0g  6658  ordgt0ge1  6698  omfnex  6712  oeiv  6719  nna0r  6741  nnm0r  6742  nnsucsssuc  6755  nn2m  6790  nnaordex  6791  nnawordex  6792  ecdmn0m  6841  ecelqsi  6853  ecidg  6863  ectocl  6866  mapfset  6935  encv  7018  f1oen  7035  ssdomg  7055  map1  7091  fiprc  7094  dom1o  7106  xpdom1  7123  fict  7160  isinfinf  7191  ac6sfi  7192  xpfi  7229  en1eqsn  7255  fidcenumlemr  7262  fiss  7301  fipwfi  7311  eqinfti  7350  djueq2  7371  djulclr  7379  djurclr  7380  djulcl  7381  djurcl  7382  djuf1olem  7383  djulclb  7385  inl11  7395  eldju1st  7401  1stinl  7404  2ndinl  7405  1stinr  7406  2ndinr  7407  ctssdccl  7441  isomnimap  7467  ismkvmap  7484  iswomnimap  7496  finacn  7550  djucomen  7562  exmidapne  7616  0nnq  7721  mulidnq  7746  archnqq  7774  prarloclemarch2  7776  nqnq0pi  7795  nq0m0r  7813  nq02m  7822  prarloclemlt  7850  prarloclemn  7856  prarloclem5  7857  addnqprllem  7884  addnqprulem  7885  appdivnq  7920  1idprl  7947  1idpru  7948  addextpr  7978  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemnbj  8024  caucvgprlemloc  8032  caucvgprprlemnbj  8050  caucvgprprlemloc  8060  caucvgprprlemaddq  8065  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemloc  8078  suplocexprlemlub  8081  0nsr  8106  ltsosr  8121  recexgt0sr  8130  prsrpos  8142  caucvgsr  8159  mappsrprg  8161  suplocsrlem  8165  mulresr  8195  axcnre  8238  axpre-ltwlin  8240  mullid  8314  0re  8316  axmulgt0  8387  ltnsym2  8406  eqlei  8409  ltnei  8419  muladd11  8449  cnegex  8494  0cnALT  8506  negcl  8516  negneg  8566  mul02  8704  mulm1  8717  lt0neg2  8787  le0neg2  8789  recexre  8896  recexgt0  8898  mulge0  8937  gt0ap0i  8945  recextlem1  8969  recexap  8971  recclapzi  9057  recap0apzi  9058  recidapzi  9059  divassapzi  9082  divmulapzi  9083  divdirapzi  9084  rerecclapzi  9096  ltp1  9164  recgt0i  9226  ltmul1i  9240  ltdiv1i  9241  ltmuldivi  9242  ltmul2i  9243  lemul1i  9244  lemul2i  9245  sup3exmid  9277  nngt1ne1  9318  nnrecre  9320  nn0ge0  9567  nn0addcl  9577  nn0mulcl  9578  zgt0ge1  9682  dfuzi  9735  eluzel2  9905  eluz2b1  9980  uz2m1nn  9984  elnn0dc  9990  elnndc  9991  nn01to3  9996  zq  10005  nnrecq  10024  rpge0  10046  rpreccl  10060  mnflt  10164  pnfnlt  10168  mnfle  10173  xrlelttr  10187  xrltletr  10188  xrletr  10189  xgepnf  10197  xlt0neg2  10220  xle0neg2  10222  xaddpnf2  10228  xaddmnf2  10230  xaddid2  10244  elioomnf  10349  ige3m2fz  10432  fzshftral  10493  ige2m1fz1  10494  1fv  10524  4fvwrd4  10525  rebtwn2zlemstep  10665  qbtwnxr  10670  btwnzge0  10713  zmodid2  10767  q2txmodxeq0  10799  frec2uzrand  10820  frecuzrdgtcl  10827  frecfzennn  10841  nn0ennn  10848  uzennn  10851  0exp  10989  sqgt0api  11040  subsq2  11062  qsqeqor  11065  bernneq  11076  faclbnd  11157  faclbnd2  11158  faclbnd3  11159  hashinfuni  11194  hashxp  11245  hashpwfi  11247  iswrdiz  11289  lsw0  11330  ccatlid  11352  s1leng  11370  s1fv  11372  s111  11377  pfx0g  11426  2shfti  11574  reim  11595  imcl  11597  crim  11601  caucvgre  11725  rennim  11746  resqrexlemdecn  11756  qabsor  11819  absimle  11828  sqrtthi  11863  sqrtcli  11864  sqrtgt0i  11865  sqrtmsqi  11866  sqrtsqi  11867  sqsqrti  11868  sqrtge0i  11869  absidi  11870  absnidi  11871  xrmaxiflemlub  11992  serclim0  12049  fsum2d  12180  fsumcnv  12182  fsumconst  12199  modfsummodlem1  12201  fsumabs  12210  binom11  12231  prodf1  12287  prodfclim1  12289  prodsnf  12337  fprod2d  12368  fprodcnv  12370  efzval  12428  eftlub  12435  efsep  12436  ef4p  12439  efgt1  12442  reef11  12444  sinf  12449  cosf  12450  efi4p  12462  sinneg  12471  cosneg  12472  efival  12477  efmival  12478  cos01gt0  12508  sin02gt0  12509  absefib  12516  efieq1re  12517  demoivre  12518  demoivreALT  12519  eirraplem  12522  0dvds  12556  odd2np1lem  12617  odd2np1  12618  even2n  12619  mod2eq0even  12623  2teven  12632  opoe  12640  omoe  12641  opeo  12642  omeo  12643  m1exp1  12646  bits0e  12694  bits0o  12695  bitsinv1  12707  gcd0id  12734  gcdid0  12735  1gcd  12747  lcmdvds  12835  isprm2lem  12872  isprm3  12874  prmgt1  12888  coprm  12900  isevengcd2  12914  isoddgcd1  12915  sqpweven  12931  2sqpwodd  12932  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem14  13034  pythagtriplem16  13036  pc2dvds  13087  oddprmdvds  13111  pockthi  13115  1arith2  13125  unennn  13266  ctinfomlemom  13296  qnnen  13300  ssnnctlemct  13315  strslfv  13375  strle1g  13437  1strbas  13448  tgval  13593  ismgmn0  13655  mulgval  13902  mulgfng  13904  mulg0  13905  mulg1  13909  mulg2  13911  isnsg  13982  ringidvalg  14239  issrg  14243  subrgpropd  14534  rrgval  14543  islmod  14600  scaffvalg  14615  islssm  14666  sraval  14746  mopnset  14861  metuex  14864  zrhval  14924  zrhvalg  14925  zrhex  14928  psrbag  14976  psrbagaddclfi  14984  istopon  15037  eltg4i  15079  eltg3  15081  tg1  15083  tg2  15084  topnex  15110  cldrcl  15126  restsn  15204  lmrcl  15216  metflem  15373  xmetf  15374  ismet2  15378  xmeteq0  15383  xmettri2  15385  xmetpsmet  15393  xmetres2  15403  blfvalps  15409  blex  15411  blvalps  15412  blval  15413  blfps  15433  blf  15434  mopnval  15466  cnbl0  15558  cnblcld  15559  blssioo  15577  resubmet  15580  cncfmet  15616  cnplimcim  15691  cnlimcim  15695  cnlimc  15696  dvfgg  15712  dvfpm  15713  dvfcnpm  15714  dvcj  15733  dvmptfsum  15749  reeff1olem  15795  ef2kpi  15830  sinperlem  15832  sin2kpi  15835  cos2kpi  15836  sinhalfpip  15844  sinhalfpim  15845  coshalfpip  15846  coshalfpim  15847  sincosq1sgn  15850  sinq12gt0  15854  sinkpi  15871  reeflog  15887  relogef  15888  logrpap0b  15900  loggt0b  15915  1cxp  15925  ecxp  15926  2logb9irrap  16002  0sgm  16013  lgsval2lem  16043  m1lgs  16118  1vgrex  16175  upgrfi  16257  umgredgnlp  16307  wlkop  16503  clwwlkn0  16563  djucllem  16742  bdrabexg  16846  bdunexb  16860  peano5set  16880  speano5  16884  bj-omtrans  16896  pw1ninf  16935  pwf1oexmid  16943  nninfsellemeq  16962  iswomninnlem  17004