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  1324  mp3an12  1327  mp3an13  1328  ax9o  1698  sbnfc2  3119  ssdifss  3267  undifss  3505  uneqdifeqim  3510  elssuni  3839  csbexa  4134  difexg  4146  rabexg  4148  abssexg  4184  snexg  4186  copsexg  4246  sotritric  4326  sotritrieq  4327  trsuc  4424  oneli  4430  unexb  4444  opeluu  4452  rabxfr  4472  reuhyp  4474  ordunisuc2r  4515  reg3exmid  4581  brrelex12i  4670  brrelex1i  4671  brrelex2i  4672  xpss2  4739  opabid2  4760  eliunxp  4768  releldmi  4868  relelrni  4869  dmexg  4893  rnexg  4894  elres  4945  resexg  4949  relbrcnvg  5009  brcodir  5018  sotri  5026  sotri2  5028  sotri3  5029  dfrel2  5081  coi1  5146  fco  5383  fssres  5393  fabexg  5405  fvopab3g  5591  mptrcl  5600  mpteqb  5608  elfvmptrab1  5612  ffvelcdmi  5652  fsn2  5692  dfmptg  5697  fvpr1  5722  fvconst2  5734  mptexg  5743  oprabid  5909  ovprc  5912  caovcl  6031  caovass  6037  caovdi  6056  elmpocl  6071  ofexg  6089  resfunexgALT  6111  fo1stresm  6164  fo2ndresm  6165  1stexg  6170  2ndexg  6171  elopabi  6198  mpoexxg  6213  mpoxopn0yelv  6242  rntpos  6260  smores  6295  tfr0dm  6325  tfrlemibxssdm  6330  tfrexlem  6337  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  rdgruledefgg  6378  rdgruledefg  6379  rdgivallem  6384  rdgexg  6392  frec0g  6400  ordgt0ge1  6438  omfnex  6452  oeiv  6459  nna0r  6481  nnm0r  6482  nnsucsssuc  6495  nn2m  6530  nnaordex  6531  nnawordex  6532  ecdmn0m  6579  ecelqsi  6591  ecidg  6601  ectocl  6604  encv  6748  f1oen  6761  ssdomg  6780  map1  6814  fiprc  6817  xpdom1  6837  fict  6870  isinfinf  6899  ac6sfi  6900  xpfi  6931  en1eqsn  6949  fidcenumlemr  6956  fiss  6978  eqinfti  7021  djueq2  7042  djulclr  7050  djurclr  7051  djulcl  7052  djurcl  7053  djuf1olem  7054  djulclb  7056  inl11  7066  eldju1st  7072  1stinl  7075  2ndinl  7076  1stinr  7077  2ndinr  7078  ctssdccl  7112  isomnimap  7137  ismkvmap  7154  iswomnimap  7166  djucomen  7217  exmidapne  7261  0nnq  7365  mulidnq  7390  archnqq  7418  prarloclemarch2  7420  nqnq0pi  7439  nq0m0r  7457  nq02m  7466  prarloclemlt  7494  prarloclemn  7500  prarloclem5  7501  addnqprllem  7528  addnqprulem  7529  appdivnq  7564  1idprl  7591  1idpru  7592  addextpr  7622  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemnbj  7668  caucvgprlemloc  7676  caucvgprprlemnbj  7694  caucvgprprlemloc  7704  caucvgprprlemaddq  7709  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemloc  7722  suplocexprlemlub  7725  0nsr  7750  ltsosr  7765  recexgt0sr  7774  prsrpos  7786  caucvgsr  7803  mappsrprg  7805  suplocsrlem  7809  mulresr  7839  axcnre  7882  axpre-ltwlin  7884  mullid  7957  0re  7959  axmulgt0  8031  ltnsym2  8050  eqlei  8053  ltnei  8063  muladd11  8092  cnegex  8137  0cnALT  8149  negcl  8159  negneg  8209  mul02  8346  mulm1  8359  lt0neg2  8428  le0neg2  8430  recexre  8537  recexgt0  8539  mulge0  8578  gt0ap0i  8586  recextlem1  8610  recexap  8612  recclapzi  8696  recap0apzi  8697  recidapzi  8698  divassapzi  8721  divmulapzi  8722  divdirapzi  8723  rerecclapzi  8735  ltp1  8803  recgt0i  8865  ltmul1i  8879  ltdiv1i  8880  ltmuldivi  8881  ltmul2i  8882  lemul1i  8883  lemul2i  8884  sup3exmid  8916  nngt1ne1  8956  nnrecre  8958  nn0ge0  9203  nn0addcl  9213  nn0mulcl  9214  zgt0ge1  9313  dfuzi  9365  eluzel2  9535  eluz2b1  9603  uz2m1nn  9607  elnn0dc  9613  elnndc  9614  nn01to3  9619  zq  9628  nnrecq  9647  rpge0  9668  rpreccl  9682  mnflt  9785  pnfnlt  9789  mnfle  9794  xrlelttr  9808  xrltletr  9809  xrletr  9810  xgepnf  9818  xlt0neg2  9841  xle0neg2  9843  xaddpnf2  9849  xaddmnf2  9851  xaddid2  9865  elioomnf  9970  ige3m2fz  10051  fzshftral  10110  ige2m1fz1  10111  1fv  10141  4fvwrd4  10142  rebtwn2zlemstep  10255  qbtwnxr  10260  btwnzge0  10302  zmodid2  10354  q2txmodxeq0  10386  frec2uzrand  10407  frecuzrdgtcl  10414  frecfzennn  10428  nn0ennn  10435  uzennn  10438  0exp  10557  sqgt0api  10608  subsq2  10630  qsqeqor  10633  bernneq  10643  faclbnd  10723  faclbnd2  10724  faclbnd3  10725  hashinfuni  10759  hashxp  10808  2shfti  10842  reim  10863  imcl  10865  crim  10869  caucvgre  10992  rennim  11013  resqrexlemdecn  11023  qabsor  11086  absimle  11095  sqrtthi  11130  sqrtcli  11131  sqrtgt0i  11132  sqrtmsqi  11133  sqrtsqi  11134  sqsqrti  11135  sqrtge0i  11136  absidi  11137  absnidi  11138  xrmaxiflemlub  11258  serclim0  11315  fsum2d  11445  fsumcnv  11447  fsumconst  11464  modfsummodlem1  11466  fsumabs  11475  binom11  11496  prodf1  11552  prodfclim1  11554  prodsnf  11602  fprod2d  11633  fprodcnv  11635  efzval  11693  eftlub  11700  efsep  11701  ef4p  11704  efgt1  11707  reef11  11709  sinf  11714  cosf  11715  efi4p  11727  sinneg  11736  cosneg  11737  efival  11742  efmival  11743  cos01gt0  11772  sin02gt0  11773  absefib  11780  efieq1re  11781  demoivre  11782  demoivreALT  11783  eirraplem  11786  0dvds  11820  odd2np1lem  11879  odd2np1  11880  even2n  11881  mod2eq0even  11885  2teven  11894  opoe  11902  omoe  11903  opeo  11904  omeo  11905  m1exp1  11908  gcd0id  11982  gcdid0  11983  1gcd  11995  lcmdvds  12081  isprm2lem  12118  isprm3  12120  prmgt1  12134  coprm  12146  isevengcd2  12160  isoddgcd1  12161  sqpweven  12177  2sqpwodd  12178  pythagtriplem12  12277  pythagtriplem13  12278  pythagtriplem14  12279  pythagtriplem16  12281  pc2dvds  12331  oddprmdvds  12354  pockthi  12358  1arith2  12368  unennn  12400  ctinfomlemom  12430  qnnen  12434  ssnnctlemct  12449  strslfv  12509  strle1g  12567  1strbas  12578  tgval  12716  ismgmn0  12782  mulgval  12991  mulgfng  12992  mulg0  12993  mulg1  12995  mulg2  12997  isnsg  13067  ringidvalg  13149  issrg  13153  subrgpropd  13374  islmod  13386  scaffvalg  13401  istopon  13598  eltg4i  13640  eltg3  13642  tg1  13644  tg2  13645  topnex  13671  cldrcl  13687  restsn  13765  lmrcl  13776  metflem  13934  xmetf  13935  ismet2  13939  xmeteq0  13944  xmettri2  13946  xmetpsmet  13954  xmetres2  13964  blfvalps  13970  blex  13972  blvalps  13973  blval  13974  blfps  13994  blf  13995  mopnval  14027  cnbl0  14119  cnblcld  14120  blssioo  14130  resubmet  14133  cncfmet  14164  cnplimcim  14221  cnlimcim  14225  cnlimc  14226  dvfgg  14242  dvfpm  14243  dvfcnpm  14244  dvcj  14258  reeff1olem  14277  ef2kpi  14312  sinperlem  14314  sin2kpi  14317  cos2kpi  14318  sinhalfpip  14326  sinhalfpim  14327  coshalfpip  14328  coshalfpim  14329  sincosq1sgn  14332  sinq12gt0  14336  sinkpi  14353  reeflog  14369  relogef  14370  logrpap0b  14382  loggt0b  14397  1cxp  14406  ecxp  14407  2logb9irrap  14480  lgsval2lem  14496  m1lgs  14537  djucllem  14637  bdrabexg  14743  bdunexb  14757  peano5set  14777  speano5  14781  bj-omtrans  14793  pwf1oexmid  14834  nninfsellemeq  14848  iswomninnlem  14882