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  1337  mp3an12  1340  mp3an13  1341  ax9o  1722  sbnfc2  3158  ssdifss  3307  undifss  3545  uneqdifeqim  3550  elssuni  3887  csbexa  4184  difexg  4196  rabexg  4198  abssexg  4237  snexg  4239  copsexg  4301  sotritric  4384  sotritrieq  4385  trsuc  4482  oneli  4488  unexb  4502  opeluu  4510  rabxfr  4530  reuhyp  4532  ordunisuc2r  4575  reg3exmid  4641  brrelex12i  4730  brrelex1i  4731  brrelex2i  4732  xpss2  4799  opabid2  4822  eliunxp  4830  releldmi  4931  relelrni  4932  dmexg  4956  rnexg  4957  elres  5009  resexg  5013  relbrcnvg  5075  brcodir  5084  sotri  5092  sotri2  5094  sotri3  5095  dfrel2  5147  coi1  5212  fco  5456  fssres  5468  fabexg  5480  fvopab3g  5670  mptrcl  5680  mpteqb  5688  elfvmptrab1  5692  ffvelcdmi  5732  fsn2  5772  dfmptg  5777  fvpr1  5806  fvconst2  5818  mptexg  5827  oprabid  5994  ovprc  5998  caovcl  6119  caovass  6125  caovdi  6144  elmpocl  6159  ofexg  6181  resfunexgALT  6211  fo1stresm  6265  fo2ndresm  6266  1stexg  6271  2ndexg  6272  elopabi  6299  mpoexxg  6314  mpoxopn0yelv  6343  rntpos  6361  smores  6396  tfr0dm  6426  tfrlemibxssdm  6431  tfrexlem  6438  tfr1onlembxssdm  6447  tfrcllembxssdm  6460  rdgruledefgg  6479  rdgruledefg  6480  rdgivallem  6485  rdgexg  6493  frec0g  6501  ordgt0ge1  6539  omfnex  6553  oeiv  6560  nna0r  6582  nnm0r  6583  nnsucsssuc  6596  nn2m  6631  nnaordex  6632  nnawordex  6633  ecdmn0m  6682  ecelqsi  6694  ecidg  6704  ectocl  6707  encv  6851  f1oen  6868  ssdomg  6888  map1  6923  fiprc  6926  xpdom1  6950  fict  6986  isinfinf  7015  ac6sfi  7016  xpfi  7050  en1eqsn  7071  fidcenumlemr  7078  fiss  7100  eqinfti  7143  djueq2  7164  djulclr  7172  djurclr  7173  djulcl  7174  djurcl  7175  djuf1olem  7176  djulclb  7178  inl11  7188  eldju1st  7194  1stinl  7197  2ndinl  7198  1stinr  7199  2ndinr  7200  ctssdccl  7234  isomnimap  7260  ismkvmap  7277  iswomnimap  7289  finacn  7342  djucomen  7354  exmidapne  7402  0nnq  7507  mulidnq  7532  archnqq  7560  prarloclemarch2  7562  nqnq0pi  7581  nq0m0r  7599  nq02m  7608  prarloclemlt  7636  prarloclemn  7642  prarloclem5  7643  addnqprllem  7670  addnqprulem  7671  appdivnq  7706  1idprl  7733  1idpru  7734  addextpr  7764  cauappcvgprlemdisj  7794  cauappcvgprlemloc  7795  cauappcvgprlemladdru  7799  cauappcvgprlemladdrl  7800  caucvgprlemnbj  7810  caucvgprlemloc  7818  caucvgprprlemnbj  7836  caucvgprprlemloc  7846  caucvgprprlemaddq  7851  suplocexprlemmu  7861  suplocexprlemru  7862  suplocexprlemloc  7864  suplocexprlemlub  7867  0nsr  7892  ltsosr  7907  recexgt0sr  7916  prsrpos  7928  caucvgsr  7945  mappsrprg  7947  suplocsrlem  7951  mulresr  7981  axcnre  8024  axpre-ltwlin  8026  mullid  8100  0re  8102  axmulgt0  8174  ltnsym2  8193  eqlei  8196  ltnei  8206  muladd11  8235  cnegex  8280  0cnALT  8292  negcl  8302  negneg  8352  mul02  8489  mulm1  8502  lt0neg2  8572  le0neg2  8574  recexre  8681  recexgt0  8683  mulge0  8722  gt0ap0i  8730  recextlem1  8754  recexap  8756  recclapzi  8840  recap0apzi  8841  recidapzi  8842  divassapzi  8865  divmulapzi  8866  divdirapzi  8867  rerecclapzi  8879  ltp1  8947  recgt0i  9009  ltmul1i  9023  ltdiv1i  9024  ltmuldivi  9025  ltmul2i  9026  lemul1i  9027  lemul2i  9028  sup3exmid  9060  nngt1ne1  9101  nnrecre  9103  nn0ge0  9350  nn0addcl  9360  nn0mulcl  9361  zgt0ge1  9461  dfuzi  9513  eluzel2  9683  eluz2b1  9752  uz2m1nn  9756  elnn0dc  9762  elnndc  9763  nn01to3  9768  zq  9777  nnrecq  9796  rpge0  9818  rpreccl  9832  mnflt  9935  pnfnlt  9939  mnfle  9944  xrlelttr  9958  xrltletr  9959  xrletr  9960  xgepnf  9968  xlt0neg2  9991  xle0neg2  9993  xaddpnf2  9999  xaddmnf2  10001  xaddid2  10015  elioomnf  10120  ige3m2fz  10201  fzshftral  10260  ige2m1fz1  10261  1fv  10291  4fvwrd4  10292  rebtwn2zlemstep  10427  qbtwnxr  10432  btwnzge0  10475  zmodid2  10529  q2txmodxeq0  10561  frec2uzrand  10582  frecuzrdgtcl  10589  frecfzennn  10603  nn0ennn  10610  uzennn  10613  0exp  10751  sqgt0api  10802  subsq2  10824  qsqeqor  10827  bernneq  10837  faclbnd  10918  faclbnd2  10919  faclbnd3  10920  hashinfuni  10954  hashxp  11003  iswrdiz  11033  lsw0  11073  ccatlid  11095  s1leng  11111  s1fv  11113  s111  11118  pfx0g  11162  2shfti  11227  reim  11248  imcl  11250  crim  11254  caucvgre  11377  rennim  11398  resqrexlemdecn  11408  qabsor  11471  absimle  11480  sqrtthi  11515  sqrtcli  11516  sqrtgt0i  11517  sqrtmsqi  11518  sqrtsqi  11519  sqsqrti  11520  sqrtge0i  11521  absidi  11522  absnidi  11523  xrmaxiflemlub  11644  serclim0  11701  fsum2d  11831  fsumcnv  11833  fsumconst  11850  modfsummodlem1  11852  fsumabs  11861  binom11  11882  prodf1  11938  prodfclim1  11940  prodsnf  11988  fprod2d  12019  fprodcnv  12021  efzval  12079  eftlub  12086  efsep  12087  ef4p  12090  efgt1  12093  reef11  12095  sinf  12100  cosf  12101  efi4p  12113  sinneg  12122  cosneg  12123  efival  12128  efmival  12129  cos01gt0  12159  sin02gt0  12160  absefib  12167  efieq1re  12168  demoivre  12169  demoivreALT  12170  eirraplem  12173  0dvds  12207  odd2np1lem  12268  odd2np1  12269  even2n  12270  mod2eq0even  12274  2teven  12283  opoe  12291  omoe  12292  opeo  12293  omeo  12294  m1exp1  12297  bits0e  12345  bits0o  12346  bitsinv1  12358  gcd0id  12385  gcdid0  12386  1gcd  12398  lcmdvds  12486  isprm2lem  12523  isprm3  12525  prmgt1  12539  coprm  12551  isevengcd2  12565  isoddgcd1  12566  sqpweven  12582  2sqpwodd  12583  pythagtriplem12  12683  pythagtriplem13  12684  pythagtriplem14  12685  pythagtriplem16  12687  pc2dvds  12738  oddprmdvds  12762  pockthi  12766  1arith2  12776  unennn  12853  ctinfomlemom  12883  qnnen  12887  ssnnctlemct  12902  strslfv  12962  strle1g  13023  1strbas  13034  tgval  13179  ismgmn0  13275  mulgval  13543  mulgfng  13545  mulg0  13546  mulg1  13550  mulg2  13552  isnsg  13623  ringidvalg  13808  issrg  13812  subrgpropd  14100  rrgval  14109  islmod  14138  scaffvalg  14153  islssm  14204  sraval  14284  mopnset  14399  metuex  14402  zrhval  14464  zrhvalg  14465  zrhex  14468  psrbag  14516  istopon  14570  eltg4i  14612  eltg3  14614  tg1  14616  tg2  14617  topnex  14643  cldrcl  14659  restsn  14737  lmrcl  14748  metflem  14906  xmetf  14907  ismet2  14911  xmeteq0  14916  xmettri2  14918  xmetpsmet  14926  xmetres2  14936  blfvalps  14942  blex  14944  blvalps  14945  blval  14946  blfps  14966  blf  14967  mopnval  14999  cnbl0  15091  cnblcld  15092  blssioo  15110  resubmet  15113  cncfmet  15149  cnplimcim  15224  cnlimcim  15228  cnlimc  15229  dvfgg  15245  dvfpm  15246  dvfcnpm  15247  dvcj  15266  dvmptfsum  15282  reeff1olem  15328  ef2kpi  15363  sinperlem  15365  sin2kpi  15368  cos2kpi  15369  sinhalfpip  15377  sinhalfpim  15378  coshalfpip  15379  coshalfpim  15380  sincosq1sgn  15383  sinq12gt0  15387  sinkpi  15404  reeflog  15420  relogef  15421  logrpap0b  15433  loggt0b  15448  1cxp  15457  ecxp  15458  2logb9irrap  15534  0sgm  15542  lgsval2lem  15572  m1lgs  15647  1vgrex  15704  upgrfi  15783  umgredgnlp  15826  djucllem  15906  bdrabexg  16011  bdunexb  16025  peano5set  16045  speano5  16049  bj-omtrans  16061  dom1o  16098  pwf1oexmid  16108  nninfsellemeq  16123  iswomninnlem  16160