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  1358  mp3an12  1361  mp3an13  1362  ax9o  1744  sbnfc2  3186  ssdifss  3335  undifss  3573  uneqdifeqim  3578  elssuni  3919  csbexa  4216  difexg  4229  rabexg  4231  abssexg  4270  snexg  4272  copsexg  4334  sotritric  4419  sotritrieq  4420  trsuc  4517  oneli  4523  unexb  4537  opeluu  4545  rabxfr  4565  reuhyp  4567  ordunisuc2r  4610  reg3exmid  4676  brrelex12i  4766  brrelex1i  4767  brrelex2i  4768  xpss2  4835  opabid2  4859  eliunxp  4867  releldmi  4969  relelrni  4970  dmexg  4994  rnexg  4995  elres  5047  resexg  5051  relbrcnvg  5113  brcodir  5122  sotri  5130  sotri2  5132  sotri3  5133  dfrel2  5185  coi1  5250  fco  5497  fssres  5509  fabexg  5521  fvopab3g  5715  mptrcl  5725  mpteqb  5733  elfvmptrab1  5737  ffvelcdmi  5777  fsn2  5817  dfmptg  5822  fcof  5828  fvpr1  5853  fvconst2  5865  mptexg  5874  oprabid  6045  ovprc  6049  caovcl  6172  caovass  6178  caovdi  6197  elmpocl  6212  relmptopab  6219  ofexg  6235  resfunexgALT  6265  fo1stresm  6319  fo2ndresm  6320  1stexg  6325  2ndexg  6326  elopabi  6355  mpoexxg  6370  elmpom  6398  mpoxopn0yelv  6400  rntpos  6418  smores  6453  tfr0dm  6483  tfrlemibxssdm  6488  tfrexlem  6495  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  rdgruledefgg  6536  rdgruledefg  6537  rdgivallem  6542  rdgexg  6550  frec0g  6558  ordgt0ge1  6598  omfnex  6612  oeiv  6619  nna0r  6641  nnm0r  6642  nnsucsssuc  6655  nn2m  6690  nnaordex  6691  nnawordex  6692  ecdmn0m  6741  ecelqsi  6753  ecidg  6763  ectocl  6766  encv  6910  f1oen  6927  ssdomg  6947  map1  6982  fiprc  6985  dom1o  6997  xpdom1  7014  fict  7050  isinfinf  7079  ac6sfi  7080  xpfi  7117  en1eqsn  7138  fidcenumlemr  7145  fiss  7167  eqinfti  7210  djueq2  7231  djulclr  7239  djurclr  7240  djulcl  7241  djurcl  7242  djuf1olem  7243  djulclb  7245  inl11  7255  eldju1st  7261  1stinl  7264  2ndinl  7265  1stinr  7266  2ndinr  7267  ctssdccl  7301  isomnimap  7327  ismkvmap  7344  iswomnimap  7356  finacn  7409  djucomen  7421  exmidapne  7469  0nnq  7574  mulidnq  7599  archnqq  7627  prarloclemarch2  7629  nqnq0pi  7648  nq0m0r  7666  nq02m  7675  prarloclemlt  7703  prarloclemn  7709  prarloclem5  7710  addnqprllem  7737  addnqprulem  7738  appdivnq  7773  1idprl  7800  1idpru  7801  addextpr  7831  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemnbj  7877  caucvgprlemloc  7885  caucvgprprlemnbj  7903  caucvgprprlemloc  7913  caucvgprprlemaddq  7918  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemloc  7931  suplocexprlemlub  7934  0nsr  7959  ltsosr  7974  recexgt0sr  7983  prsrpos  7995  caucvgsr  8012  mappsrprg  8014  suplocsrlem  8018  mulresr  8048  axcnre  8091  axpre-ltwlin  8093  mullid  8167  0re  8169  axmulgt0  8241  ltnsym2  8260  eqlei  8263  ltnei  8273  muladd11  8302  cnegex  8347  0cnALT  8359  negcl  8369  negneg  8419  mul02  8556  mulm1  8569  lt0neg2  8639  le0neg2  8641  recexre  8748  recexgt0  8750  mulge0  8789  gt0ap0i  8797  recextlem1  8821  recexap  8823  recclapzi  8907  recap0apzi  8908  recidapzi  8909  divassapzi  8932  divmulapzi  8933  divdirapzi  8934  rerecclapzi  8946  ltp1  9014  recgt0i  9076  ltmul1i  9090  ltdiv1i  9091  ltmuldivi  9092  ltmul2i  9093  lemul1i  9094  lemul2i  9095  sup3exmid  9127  nngt1ne1  9168  nnrecre  9170  nn0ge0  9417  nn0addcl  9427  nn0mulcl  9428  zgt0ge1  9528  dfuzi  9580  eluzel2  9750  eluz2b1  9825  uz2m1nn  9829  elnn0dc  9835  elnndc  9836  nn01to3  9841  zq  9850  nnrecq  9869  rpge0  9891  rpreccl  9905  mnflt  10008  pnfnlt  10012  mnfle  10017  xrlelttr  10031  xrltletr  10032  xrletr  10033  xgepnf  10041  xlt0neg2  10064  xle0neg2  10066  xaddpnf2  10072  xaddmnf2  10074  xaddid2  10088  elioomnf  10193  ige3m2fz  10274  fzshftral  10333  ige2m1fz1  10334  1fv  10364  4fvwrd4  10365  rebtwn2zlemstep  10502  qbtwnxr  10507  btwnzge0  10550  zmodid2  10604  q2txmodxeq0  10636  frec2uzrand  10657  frecuzrdgtcl  10664  frecfzennn  10678  nn0ennn  10685  uzennn  10688  0exp  10826  sqgt0api  10877  subsq2  10899  qsqeqor  10902  bernneq  10912  faclbnd  10993  faclbnd2  10994  faclbnd3  10995  hashinfuni  11029  hashxp  11080  iswrdiz  11110  lsw0  11151  ccatlid  11173  s1leng  11191  s1fv  11193  s111  11198  pfx0g  11247  2shfti  11382  reim  11403  imcl  11405  crim  11409  caucvgre  11532  rennim  11553  resqrexlemdecn  11563  qabsor  11626  absimle  11635  sqrtthi  11670  sqrtcli  11671  sqrtgt0i  11672  sqrtmsqi  11673  sqrtsqi  11674  sqsqrti  11675  sqrtge0i  11676  absidi  11677  absnidi  11678  xrmaxiflemlub  11799  serclim0  11856  fsum2d  11986  fsumcnv  11988  fsumconst  12005  modfsummodlem1  12007  fsumabs  12016  binom11  12037  prodf1  12093  prodfclim1  12095  prodsnf  12143  fprod2d  12174  fprodcnv  12176  efzval  12234  eftlub  12241  efsep  12242  ef4p  12245  efgt1  12248  reef11  12250  sinf  12255  cosf  12256  efi4p  12268  sinneg  12277  cosneg  12278  efival  12283  efmival  12284  cos01gt0  12314  sin02gt0  12315  absefib  12322  efieq1re  12323  demoivre  12324  demoivreALT  12325  eirraplem  12328  0dvds  12362  odd2np1lem  12423  odd2np1  12424  even2n  12425  mod2eq0even  12429  2teven  12438  opoe  12446  omoe  12447  opeo  12448  omeo  12449  m1exp1  12452  bits0e  12500  bits0o  12501  bitsinv1  12513  gcd0id  12540  gcdid0  12541  1gcd  12553  lcmdvds  12641  isprm2lem  12678  isprm3  12680  prmgt1  12694  coprm  12706  isevengcd2  12720  isoddgcd1  12721  sqpweven  12737  2sqpwodd  12738  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem14  12840  pythagtriplem16  12842  pc2dvds  12893  oddprmdvds  12917  pockthi  12921  1arith2  12931  unennn  13008  ctinfomlemom  13038  qnnen  13042  ssnnctlemct  13057  strslfv  13117  strle1g  13179  1strbas  13190  tgval  13335  ismgmn0  13431  mulgval  13699  mulgfng  13701  mulg0  13702  mulg1  13706  mulg2  13708  isnsg  13779  ringidvalg  13964  issrg  13968  subrgpropd  14257  rrgval  14266  islmod  14295  scaffvalg  14310  islssm  14361  sraval  14441  mopnset  14556  metuex  14559  zrhval  14621  zrhvalg  14622  zrhex  14625  psrbag  14673  istopon  14727  eltg4i  14769  eltg3  14771  tg1  14773  tg2  14774  topnex  14800  cldrcl  14816  restsn  14894  lmrcl  14906  metflem  15063  xmetf  15064  ismet2  15068  xmeteq0  15073  xmettri2  15075  xmetpsmet  15083  xmetres2  15093  blfvalps  15099  blex  15101  blvalps  15102  blval  15103  blfps  15123  blf  15124  mopnval  15156  cnbl0  15248  cnblcld  15249  blssioo  15267  resubmet  15270  cncfmet  15306  cnplimcim  15381  cnlimcim  15385  cnlimc  15386  dvfgg  15402  dvfpm  15403  dvfcnpm  15404  dvcj  15423  dvmptfsum  15439  reeff1olem  15485  ef2kpi  15520  sinperlem  15522  sin2kpi  15525  cos2kpi  15526  sinhalfpip  15534  sinhalfpim  15535  coshalfpip  15536  coshalfpim  15537  sincosq1sgn  15540  sinq12gt0  15544  sinkpi  15561  reeflog  15577  relogef  15578  logrpap0b  15590  loggt0b  15605  1cxp  15614  ecxp  15615  2logb9irrap  15691  0sgm  15699  lgsval2lem  15729  m1lgs  15804  1vgrex  15861  upgrfi  15943  umgredgnlp  15991  wlkop  16145  clwwlkn0  16203  djucllem  16332  bdrabexg  16437  bdunexb  16451  peano5set  16471  speano5  16475  bj-omtrans  16487  pw1ninf  16526  pwf1oexmid  16536  nninfsellemeq  16552  iswomninnlem  16589