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  1360  mp3an12  1363  mp3an13  1364  ax9o  1745  sbnfc2  3187  ssdifss  3336  undifss  3574  uneqdifeqim  3579  elssuni  3920  csbexa  4217  difexg  4230  rabexg  4232  abssexg  4271  snexg  4273  copsexg  4335  sotritric  4420  sotritrieq  4421  trsuc  4518  oneli  4524  unexb  4538  opeluu  4546  rabxfr  4566  reuhyp  4568  ordunisuc2r  4611  reg3exmid  4677  brrelex12i  4767  brrelex1i  4768  brrelex2i  4769  xpss2  4836  opabid2  4860  eliunxp  4868  releldmi  4970  relelrni  4971  dmexg  4995  rnexg  4996  elres  5048  resexg  5052  relbrcnvg  5114  brcodir  5123  sotri  5131  sotri2  5133  sotri3  5134  dfrel2  5186  coi1  5251  fco  5499  fssres  5511  fabexg  5523  fvopab3g  5719  mptrcl  5729  mpteqb  5737  elfvmptrab1  5741  ffvelcdmi  5781  fsn2  5821  dfmptg  5827  fcof  5833  fvpr1  5858  fvconst2  5870  mptexg  5881  oprabid  6052  ovprc  6056  caovcl  6179  caovass  6185  caovdi  6204  elmpocl  6219  relmptopab  6226  ofexg  6242  resfunexgALT  6272  fo1stresm  6326  fo2ndresm  6327  1stexg  6332  2ndexg  6333  elopabi  6362  mpoexxg  6377  elmpom  6405  mpoxopn0yelv  6407  rntpos  6425  smores  6460  tfr0dm  6490  tfrlemibxssdm  6495  tfrexlem  6502  tfr1onlembxssdm  6511  tfrcllembxssdm  6524  rdgruledefgg  6543  rdgruledefg  6544  rdgivallem  6549  rdgexg  6557  frec0g  6565  ordgt0ge1  6605  omfnex  6619  oeiv  6626  nna0r  6648  nnm0r  6649  nnsucsssuc  6662  nn2m  6697  nnaordex  6698  nnawordex  6699  ecdmn0m  6748  ecelqsi  6760  ecidg  6770  ectocl  6773  encv  6917  f1oen  6934  ssdomg  6954  map1  6989  fiprc  6992  dom1o  7004  xpdom1  7021  fict  7057  isinfinf  7088  ac6sfi  7089  xpfi  7126  en1eqsn  7149  fidcenumlemr  7156  fiss  7178  eqinfti  7221  djueq2  7242  djulclr  7250  djurclr  7251  djulcl  7252  djurcl  7253  djuf1olem  7254  djulclb  7256  inl11  7266  eldju1st  7272  1stinl  7275  2ndinl  7276  1stinr  7277  2ndinr  7278  ctssdccl  7312  isomnimap  7338  ismkvmap  7355  iswomnimap  7367  finacn  7421  djucomen  7433  exmidapne  7481  0nnq  7586  mulidnq  7611  archnqq  7639  prarloclemarch2  7641  nqnq0pi  7660  nq0m0r  7678  nq02m  7687  prarloclemlt  7715  prarloclemn  7721  prarloclem5  7722  addnqprllem  7749  addnqprulem  7750  appdivnq  7785  1idprl  7812  1idpru  7813  addextpr  7843  cauappcvgprlemdisj  7873  cauappcvgprlemloc  7874  cauappcvgprlemladdru  7878  cauappcvgprlemladdrl  7879  caucvgprlemnbj  7889  caucvgprlemloc  7897  caucvgprprlemnbj  7915  caucvgprprlemloc  7925  caucvgprprlemaddq  7930  suplocexprlemmu  7940  suplocexprlemru  7941  suplocexprlemloc  7943  suplocexprlemlub  7946  0nsr  7971  ltsosr  7986  recexgt0sr  7995  prsrpos  8007  caucvgsr  8024  mappsrprg  8026  suplocsrlem  8030  mulresr  8060  axcnre  8103  axpre-ltwlin  8105  mullid  8179  0re  8181  axmulgt0  8253  ltnsym2  8272  eqlei  8275  ltnei  8285  muladd11  8314  cnegex  8359  0cnALT  8371  negcl  8381  negneg  8431  mul02  8568  mulm1  8581  lt0neg2  8651  le0neg2  8653  recexre  8760  recexgt0  8762  mulge0  8801  gt0ap0i  8809  recextlem1  8833  recexap  8835  recclapzi  8919  recap0apzi  8920  recidapzi  8921  divassapzi  8944  divmulapzi  8945  divdirapzi  8946  rerecclapzi  8958  ltp1  9026  recgt0i  9088  ltmul1i  9102  ltdiv1i  9103  ltmuldivi  9104  ltmul2i  9105  lemul1i  9106  lemul2i  9107  sup3exmid  9139  nngt1ne1  9180  nnrecre  9182  nn0ge0  9429  nn0addcl  9439  nn0mulcl  9440  zgt0ge1  9540  dfuzi  9592  eluzel2  9762  eluz2b1  9837  uz2m1nn  9841  elnn0dc  9847  elnndc  9848  nn01to3  9853  zq  9862  nnrecq  9881  rpge0  9903  rpreccl  9917  mnflt  10020  pnfnlt  10024  mnfle  10029  xrlelttr  10043  xrltletr  10044  xrletr  10045  xgepnf  10053  xlt0neg2  10076  xle0neg2  10078  xaddpnf2  10084  xaddmnf2  10086  xaddid2  10100  elioomnf  10205  ige3m2fz  10286  fzshftral  10345  ige2m1fz1  10346  1fv  10376  4fvwrd4  10377  rebtwn2zlemstep  10515  qbtwnxr  10520  btwnzge0  10563  zmodid2  10617  q2txmodxeq0  10649  frec2uzrand  10670  frecuzrdgtcl  10677  frecfzennn  10691  nn0ennn  10698  uzennn  10701  0exp  10839  sqgt0api  10890  subsq2  10912  qsqeqor  10915  bernneq  10925  faclbnd  11006  faclbnd2  11007  faclbnd3  11008  hashinfuni  11042  hashxp  11093  iswrdiz  11126  lsw0  11167  ccatlid  11189  s1leng  11207  s1fv  11209  s111  11214  pfx0g  11263  2shfti  11411  reim  11432  imcl  11434  crim  11438  caucvgre  11561  rennim  11582  resqrexlemdecn  11592  qabsor  11655  absimle  11664  sqrtthi  11699  sqrtcli  11700  sqrtgt0i  11701  sqrtmsqi  11702  sqrtsqi  11703  sqsqrti  11704  sqrtge0i  11705  absidi  11706  absnidi  11707  xrmaxiflemlub  11828  serclim0  11885  fsum2d  12016  fsumcnv  12018  fsumconst  12035  modfsummodlem1  12037  fsumabs  12046  binom11  12067  prodf1  12123  prodfclim1  12125  prodsnf  12173  fprod2d  12204  fprodcnv  12206  efzval  12264  eftlub  12271  efsep  12272  ef4p  12275  efgt1  12278  reef11  12280  sinf  12285  cosf  12286  efi4p  12298  sinneg  12307  cosneg  12308  efival  12313  efmival  12314  cos01gt0  12344  sin02gt0  12345  absefib  12352  efieq1re  12353  demoivre  12354  demoivreALT  12355  eirraplem  12358  0dvds  12392  odd2np1lem  12453  odd2np1  12454  even2n  12455  mod2eq0even  12459  2teven  12468  opoe  12476  omoe  12477  opeo  12478  omeo  12479  m1exp1  12482  bits0e  12530  bits0o  12531  bitsinv1  12543  gcd0id  12570  gcdid0  12571  1gcd  12583  lcmdvds  12671  isprm2lem  12708  isprm3  12710  prmgt1  12724  coprm  12736  isevengcd2  12750  isoddgcd1  12751  sqpweven  12767  2sqpwodd  12768  pythagtriplem12  12868  pythagtriplem13  12869  pythagtriplem14  12870  pythagtriplem16  12872  pc2dvds  12923  oddprmdvds  12947  pockthi  12951  1arith2  12961  unennn  13038  ctinfomlemom  13068  qnnen  13072  ssnnctlemct  13087  strslfv  13147  strle1g  13209  1strbas  13220  tgval  13365  ismgmn0  13461  mulgval  13729  mulgfng  13731  mulg0  13732  mulg1  13736  mulg2  13738  isnsg  13809  ringidvalg  13995  issrg  13999  subrgpropd  14288  rrgval  14297  islmod  14326  scaffvalg  14341  islssm  14392  sraval  14472  mopnset  14587  metuex  14590  zrhval  14652  zrhvalg  14653  zrhex  14656  psrbag  14704  istopon  14763  eltg4i  14805  eltg3  14807  tg1  14809  tg2  14810  topnex  14836  cldrcl  14852  restsn  14930  lmrcl  14942  metflem  15099  xmetf  15100  ismet2  15104  xmeteq0  15109  xmettri2  15111  xmetpsmet  15119  xmetres2  15129  blfvalps  15135  blex  15137  blvalps  15138  blval  15139  blfps  15159  blf  15160  mopnval  15192  cnbl0  15284  cnblcld  15285  blssioo  15303  resubmet  15306  cncfmet  15342  cnplimcim  15417  cnlimcim  15421  cnlimc  15422  dvfgg  15438  dvfpm  15439  dvfcnpm  15440  dvcj  15459  dvmptfsum  15475  reeff1olem  15521  ef2kpi  15556  sinperlem  15558  sin2kpi  15561  cos2kpi  15562  sinhalfpip  15570  sinhalfpim  15571  coshalfpip  15572  coshalfpim  15573  sincosq1sgn  15576  sinq12gt0  15580  sinkpi  15597  reeflog  15613  relogef  15614  logrpap0b  15626  loggt0b  15641  1cxp  15650  ecxp  15651  2logb9irrap  15727  0sgm  15735  lgsval2lem  15765  m1lgs  15840  1vgrex  15897  upgrfi  15979  umgredgnlp  16029  wlkop  16225  clwwlkn0  16285  djucllem  16454  bdrabexg  16559  bdunexb  16573  peano5set  16593  speano5  16597  bj-omtrans  16609  pw1ninf  16648  pwf1oexmid  16658  nninfsellemeq  16674  iswomninnlem  16716