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  4262  difexg  4275  rabexg  4279  abssexg  4319  snexg  4321  copsexg  4384  sotritric  4469  sotritrieq  4470  trsuc  4567  oneli  4573  unexb  4588  opeluu  4596  rabxfr  4616  reuhyp  4618  ordunisuc2r  4661  reg3exmid  4727  brrelex12i  4817  brrelex1i  4818  brrelex2i  4819  xpss2  4886  opabid2  4911  eliunxp  4919  releldmi  5021  relelrni  5022  dmexg  5046  rnexg  5047  elres  5099  resexg  5103  relbrcnvg  5166  brcodir  5175  sotri  5183  sotri2  5185  sotri3  5186  dfrel2  5238  coi1  5303  fco  5552  fssres  5565  fabexg  5579  fvopab3g  5778  mptrcl  5788  mpteqb  5796  elfvmptrab1  5801  fvopab4ndm  5803  ffvelcdmi  5842  fsn2  5882  dfmptg  5888  fcof  5894  fvpr1  5919  fvconst2  5931  mptexg  5942  oprabid  6117  ovprc  6121  caovcl  6244  caovass  6250  caovdi  6269  elmpocl  6284  relmptopab  6291  ofexg  6307  resfunexgALT  6337  fo1stresm  6395  fo2ndresm  6396  1stexg  6401  2ndexg  6402  elopabi  6431  mpoexxg  6446  elmpom  6474  supp0  6478  mpoxopn0yelv  6510  rntpos  6528  smores  6563  tfr0dm  6593  tfrlemibxssdm  6598  tfrexlem  6605  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  rdgruledefgg  6646  rdgruledefg  6647  rdgivallem  6652  rdgexg  6660  frec0g  6668  ordgt0ge1  6708  omfnex  6722  oeiv  6729  nna0r  6751  nnm0r  6752  nnsucsssuc  6765  nn2m  6800  nnaordex  6801  nnawordex  6802  ecdmn0m  6851  ecelqsi  6863  ecidg  6873  ectocl  6876  mapfset  6945  encv  7028  f1oen  7045  ssdomg  7065  map1  7101  fiprc  7104  dom1o  7116  xpdom1  7133  fict  7170  isinfinf  7201  ac6sfi  7202  xpfi  7239  en1eqsn  7265  fidcenumlemr  7272  fiss  7311  fipwfi  7322  eqinfti  7361  djueq2  7382  djulclr  7390  djurclr  7391  djulcl  7392  djurcl  7393  djuf1olem  7394  djulclb  7396  inl11  7406  eldju1st  7412  1stinl  7415  2ndinl  7416  1stinr  7417  2ndinr  7418  ctssdccl  7452  isomnimap  7478  ismkvmap  7495  iswomnimap  7507  finacn  7561  djucomen  7573  exmidapne  7627  0nnq  7732  mulidnq  7757  archnqq  7785  prarloclemarch2  7787  nqnq0pi  7806  nq0m0r  7824  nq02m  7833  prarloclemlt  7861  prarloclemn  7867  prarloclem5  7868  addnqprllem  7895  addnqprulem  7896  appdivnq  7931  1idprl  7958  1idpru  7959  addextpr  7989  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemnbj  8035  caucvgprlemloc  8043  caucvgprprlemnbj  8061  caucvgprprlemloc  8071  caucvgprprlemaddq  8076  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemloc  8089  suplocexprlemlub  8092  0nsr  8117  ltsosr  8132  recexgt0sr  8141  prsrpos  8153  caucvgsr  8170  mappsrprg  8172  suplocsrlem  8176  mulresr  8206  axcnre  8249  axpre-ltwlin  8251  mullid  8325  0re  8327  axmulgt0  8398  ltnsym2  8417  eqlei  8421  ltnei  8431  muladd11  8461  cnegex  8506  0cnALT  8518  negcl  8528  negneg  8578  mul02  8716  mulm1  8729  lt0neg2  8799  le0neg2  8801  recexre  8909  recexgt0  8911  mulge0  8950  gt0ap0i  8958  recextlem1  8982  recexap  8984  recclapzi  9070  recap0apzi  9071  recidapzi  9072  divassapzi  9095  divmulapzi  9096  divdirapzi  9097  rerecclapzi  9109  ltp1  9177  recgt0i  9239  ltmul1i  9253  ltdiv1i  9254  ltmuldivi  9255  ltmul2i  9256  lemul1i  9257  lemul2i  9258  sup3exmid  9290  nngt1ne1  9342  nnrecre  9344  nn0ge0  9593  nn0addcl  9603  nn0mulcl  9604  zgt0ge1  9708  dfuzi  9761  eluzel2  9936  eluz2b1  10011  uz2m1nn  10015  elnn0dc  10021  elnndc  10022  nn01to3  10027  zq  10036  nnrecq  10055  rpge0  10078  rpreccl  10092  mnflt  10196  pnfnlt  10200  mnfle  10205  xrlelttr  10219  xrltletr  10220  xrletr  10221  xgepnf  10229  xlt0neg2  10252  xle0neg2  10254  xaddpnf2  10260  xaddmnf2  10262  xaddid2  10276  elioomnf  10381  ige3m2fz  10465  fzshftral  10526  ige2m1fz1  10527  1fv  10557  4fvwrd4  10558  rebtwn2zlemstep  10698  qbtwnxr  10703  btwnzge0  10750  zmodid2  10804  q2txmodxeq0  10836  frec2uzrand  10857  frecuzrdgtcl  10864  frecfzennn  10878  nn0ennn  10885  uzennn  10888  0exp  11026  sqgt0api  11077  subsq2  11099  qsqeqor  11102  bernneq  11113  faclbnd  11195  faclbnd2  11196  faclbnd3  11197  hashinfuni  11232  hashxp  11283  hashpwfi  11285  iswrdiz  11327  lsw0  11368  ccatlid  11390  s1leng  11408  s1fv  11410  s111  11415  pfx0g  11464  2shfti  11612  reim  11633  imcl  11635  crim  11639  caucvgre  11763  rennim  11784  resqrexlemdecn  11794  qabsor  11857  absimle  11867  sqrtthi  11902  sqrtcli  11903  sqrtgt0i  11904  sqrtmsqi  11905  sqrtsqi  11906  sqsqrti  11907  sqrtge0i  11908  absidi  11909  absnidi  11910  xrmaxiflemlub  12033  serclim0  12090  fsum2d  12221  fsumcnv  12223  fsumconst  12240  modfsummodlem1  12242  fsumabs  12251  binom11  12272  prodf1  12328  prodfclim1  12330  prodsnf  12378  fprod2d  12409  fprodcnv  12411  efzval  12469  eftlub  12476  efsep  12477  ef4p  12480  efgt1  12483  reef11  12485  sinf  12490  cosf  12491  efi4p  12503  sinneg  12512  cosneg  12513  efival  12518  efmival  12519  cos01gt0  12549  sin02gt0  12550  absefib  12557  efieq1re  12558  demoivre  12559  demoivreALT  12560  eirraplem  12563  0dvds  12597  odd2np1lem  12658  odd2np1  12659  even2n  12660  mod2eq0even  12664  2teven  12673  opoe  12681  omoe  12682  opeo  12683  omeo  12684  m1exp1  12687  bits0e  12735  bits0o  12736  bitsinv1  12748  gcd0id  12775  gcdid0  12776  1gcd  12788  lcmdvds  12876  isprm2lem  12913  isprm3  12915  prmgt1  12930  coprm  12942  isevengcd2  12956  isoddgcd1  12957  sqpweven  12974  2sqpwodd  12975  sqrtrirr  13008  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem14  13079  pythagtriplem16  13081  pc2dvds  13132  oddprmdvds  13156  pockthi  13160  1arith2  13170  prmlem1a  13244  unennn  13340  ctinfomlemom  13370  qnnen  13374  ssnnctlemct  13389  strslfv  13449  slotm  13467  strle1g  13513  1strbas  13524  tgval  13669  ismgmn0  13731  mulgval  13978  mulgfng  13980  mulg0  13981  mulg1  13985  mulg2  13987  isnsg  14058  cntrval  14145  mgpplusg  14306  mgpbas  14309  ringidvalg  14348  ringidval  14349  issrg  14353  subrgpropd  14645  rrgval  14654  islmod  14711  scaffvalg  14727  islssm  14778  sraval  14858  mopnset  14973  metuex  14976  zrhval  15036  zrhvalg  15037  zrhex  15040  asclfval  15105  psrbag  15137  psrbagaddclfi  15145  istopon  15205  eltg4i  15247  eltg3  15249  tg1  15251  tg2  15252  topnex  15278  cldrcl  15294  restsn  15372  lmrcl  15384  metflem  15541  xmetf  15542  ismet2  15546  xmeteq0  15551  xmettri2  15553  xmetpsmet  15561  xmetres2  15571  blfvalps  15577  blex  15579  blvalps  15580  blval  15581  blfps  15601  blf  15602  mopnval  15634  cnbl0  15726  cnblcld  15727  blssioo  15745  resubmet  15748  cncfmet  15784  cnplimcim  15859  cnlimcim  15863  cnlimc  15864  dvfgg  15880  dvfpm  15881  dvfcnpm  15882  dvcj  15901  dvmptfsum  15917  reeff1olem  15963  ef2kpi  15999  sinperlem  16001  sin2kpi  16004  cos2kpi  16005  sinhalfpip  16013  sinhalfpim  16014  coshalfpip  16015  coshalfpim  16016  sincosq1sgn  16019  sinq12gt0  16023  sinkpi  16040  reeflog  16056  relogef  16057  logrpap0b  16070  loggt0b  16085  1cxp  16097  ecxp  16098  2logb9irrap  16174  log2tlbndlog2  16181  log2ublem2  16183  0sgm  16215  chtublem  16256  pcbcctr  16264  bcp1ctr  16267  bclbnd  16268  bposlem1  16272  lgsval2lem  16295  m1lgs  16370  1vgrex  16427  upgrfi  16509  umgredgnlp  16559  wlkop  16755  clwwlkn0  16815  djucllem  16994  bdrabexg  17098  bdunexb  17112  peano5set  17132  speano5  17136  bj-omtrans  17148  pw1ninf  17187  pwf1oexmid  17195  nninfsellemeq  17223  iswomninnlem  17266