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  1336  mp3an12  1339  mp3an13  1340  ax9o  1720  sbnfc2  3153  ssdifss  3302  undifss  3540  uneqdifeqim  3545  elssuni  3877  csbexa  4172  difexg  4184  rabexg  4186  abssexg  4225  snexg  4227  copsexg  4287  sotritric  4370  sotritrieq  4371  trsuc  4468  oneli  4474  unexb  4488  opeluu  4496  rabxfr  4516  reuhyp  4518  ordunisuc2r  4561  reg3exmid  4627  brrelex12i  4716  brrelex1i  4717  brrelex2i  4718  xpss2  4785  opabid2  4808  eliunxp  4816  releldmi  4916  relelrni  4917  dmexg  4941  rnexg  4942  elres  4994  resexg  4998  relbrcnvg  5060  brcodir  5069  sotri  5077  sotri2  5079  sotri3  5080  dfrel2  5132  coi1  5197  fco  5440  fssres  5450  fabexg  5462  fvopab3g  5651  mptrcl  5661  mpteqb  5669  elfvmptrab1  5673  ffvelcdmi  5713  fsn2  5753  dfmptg  5758  fvpr1  5787  fvconst2  5799  mptexg  5808  oprabid  5975  ovprc  5979  caovcl  6100  caovass  6106  caovdi  6125  elmpocl  6140  ofexg  6162  resfunexgALT  6192  fo1stresm  6246  fo2ndresm  6247  1stexg  6252  2ndexg  6253  elopabi  6280  mpoexxg  6295  mpoxopn0yelv  6324  rntpos  6342  smores  6377  tfr0dm  6407  tfrlemibxssdm  6412  tfrexlem  6419  tfr1onlembxssdm  6428  tfrcllembxssdm  6441  rdgruledefgg  6460  rdgruledefg  6461  rdgivallem  6466  rdgexg  6474  frec0g  6482  ordgt0ge1  6520  omfnex  6534  oeiv  6541  nna0r  6563  nnm0r  6564  nnsucsssuc  6577  nn2m  6612  nnaordex  6613  nnawordex  6614  ecdmn0m  6663  ecelqsi  6675  ecidg  6685  ectocl  6688  encv  6832  f1oen  6849  ssdomg  6869  map1  6903  fiprc  6906  xpdom1  6929  fict  6964  isinfinf  6993  ac6sfi  6994  xpfi  7028  en1eqsn  7049  fidcenumlemr  7056  fiss  7078  eqinfti  7121  djueq2  7142  djulclr  7150  djurclr  7151  djulcl  7152  djurcl  7153  djuf1olem  7154  djulclb  7156  inl11  7166  eldju1st  7172  1stinl  7175  2ndinl  7176  1stinr  7177  2ndinr  7178  ctssdccl  7212  isomnimap  7238  ismkvmap  7255  iswomnimap  7267  finacn  7315  djucomen  7327  exmidapne  7371  0nnq  7476  mulidnq  7501  archnqq  7529  prarloclemarch2  7531  nqnq0pi  7550  nq0m0r  7568  nq02m  7577  prarloclemlt  7605  prarloclemn  7611  prarloclem5  7612  addnqprllem  7639  addnqprulem  7640  appdivnq  7675  1idprl  7702  1idpru  7703  addextpr  7733  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemnbj  7779  caucvgprlemloc  7787  caucvgprprlemnbj  7805  caucvgprprlemloc  7815  caucvgprprlemaddq  7820  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemloc  7833  suplocexprlemlub  7836  0nsr  7861  ltsosr  7876  recexgt0sr  7885  prsrpos  7897  caucvgsr  7914  mappsrprg  7916  suplocsrlem  7920  mulresr  7950  axcnre  7993  axpre-ltwlin  7995  mullid  8069  0re  8071  axmulgt0  8143  ltnsym2  8162  eqlei  8165  ltnei  8175  muladd11  8204  cnegex  8249  0cnALT  8261  negcl  8271  negneg  8321  mul02  8458  mulm1  8471  lt0neg2  8541  le0neg2  8543  recexre  8650  recexgt0  8652  mulge0  8691  gt0ap0i  8699  recextlem1  8723  recexap  8725  recclapzi  8809  recap0apzi  8810  recidapzi  8811  divassapzi  8834  divmulapzi  8835  divdirapzi  8836  rerecclapzi  8848  ltp1  8916  recgt0i  8978  ltmul1i  8992  ltdiv1i  8993  ltmuldivi  8994  ltmul2i  8995  lemul1i  8996  lemul2i  8997  sup3exmid  9029  nngt1ne1  9070  nnrecre  9072  nn0ge0  9319  nn0addcl  9329  nn0mulcl  9330  zgt0ge1  9430  dfuzi  9482  eluzel2  9652  eluz2b1  9721  uz2m1nn  9725  elnn0dc  9731  elnndc  9732  nn01to3  9737  zq  9746  nnrecq  9765  rpge0  9787  rpreccl  9801  mnflt  9904  pnfnlt  9908  mnfle  9913  xrlelttr  9927  xrltletr  9928  xrletr  9929  xgepnf  9937  xlt0neg2  9960  xle0neg2  9962  xaddpnf2  9968  xaddmnf2  9970  xaddid2  9984  elioomnf  10089  ige3m2fz  10170  fzshftral  10229  ige2m1fz1  10230  1fv  10260  4fvwrd4  10261  rebtwn2zlemstep  10393  qbtwnxr  10398  btwnzge0  10441  zmodid2  10495  q2txmodxeq0  10527  frec2uzrand  10548  frecuzrdgtcl  10555  frecfzennn  10569  nn0ennn  10576  uzennn  10579  0exp  10717  sqgt0api  10768  subsq2  10790  qsqeqor  10793  bernneq  10803  faclbnd  10884  faclbnd2  10885  faclbnd3  10886  hashinfuni  10920  hashxp  10969  iswrdiz  10999  lsw0  11039  ccatlid  11060  2shfti  11084  reim  11105  imcl  11107  crim  11111  caucvgre  11234  rennim  11255  resqrexlemdecn  11265  qabsor  11328  absimle  11337  sqrtthi  11372  sqrtcli  11373  sqrtgt0i  11374  sqrtmsqi  11375  sqrtsqi  11376  sqsqrti  11377  sqrtge0i  11378  absidi  11379  absnidi  11380  xrmaxiflemlub  11501  serclim0  11558  fsum2d  11688  fsumcnv  11690  fsumconst  11707  modfsummodlem1  11709  fsumabs  11718  binom11  11739  prodf1  11795  prodfclim1  11797  prodsnf  11845  fprod2d  11876  fprodcnv  11878  efzval  11936  eftlub  11943  efsep  11944  ef4p  11947  efgt1  11950  reef11  11952  sinf  11957  cosf  11958  efi4p  11970  sinneg  11979  cosneg  11980  efival  11985  efmival  11986  cos01gt0  12016  sin02gt0  12017  absefib  12024  efieq1re  12025  demoivre  12026  demoivreALT  12027  eirraplem  12030  0dvds  12064  odd2np1lem  12125  odd2np1  12126  even2n  12127  mod2eq0even  12131  2teven  12140  opoe  12148  omoe  12149  opeo  12150  omeo  12151  m1exp1  12154  bits0e  12202  bits0o  12203  bitsinv1  12215  gcd0id  12242  gcdid0  12243  1gcd  12255  lcmdvds  12343  isprm2lem  12380  isprm3  12382  prmgt1  12396  coprm  12408  isevengcd2  12422  isoddgcd1  12423  sqpweven  12439  2sqpwodd  12440  pythagtriplem12  12540  pythagtriplem13  12541  pythagtriplem14  12542  pythagtriplem16  12544  pc2dvds  12595  oddprmdvds  12619  pockthi  12623  1arith2  12633  unennn  12710  ctinfomlemom  12740  qnnen  12744  ssnnctlemct  12759  strslfv  12819  strle1g  12880  1strbas  12891  tgval  13036  ismgmn0  13132  mulgval  13400  mulgfng  13402  mulg0  13403  mulg1  13407  mulg2  13409  isnsg  13480  ringidvalg  13665  issrg  13669  subrgpropd  13957  rrgval  13966  islmod  13995  scaffvalg  14010  islssm  14061  sraval  14141  mopnset  14256  metuex  14259  zrhval  14321  zrhvalg  14322  zrhex  14325  psrbag  14373  istopon  14427  eltg4i  14469  eltg3  14471  tg1  14473  tg2  14474  topnex  14500  cldrcl  14516  restsn  14594  lmrcl  14605  metflem  14763  xmetf  14764  ismet2  14768  xmeteq0  14773  xmettri2  14775  xmetpsmet  14783  xmetres2  14793  blfvalps  14799  blex  14801  blvalps  14802  blval  14803  blfps  14823  blf  14824  mopnval  14856  cnbl0  14948  cnblcld  14949  blssioo  14967  resubmet  14970  cncfmet  15006  cnplimcim  15081  cnlimcim  15085  cnlimc  15086  dvfgg  15102  dvfpm  15103  dvfcnpm  15104  dvcj  15123  dvmptfsum  15139  reeff1olem  15185  ef2kpi  15220  sinperlem  15222  sin2kpi  15225  cos2kpi  15226  sinhalfpip  15234  sinhalfpim  15235  coshalfpip  15236  coshalfpim  15237  sincosq1sgn  15240  sinq12gt0  15244  sinkpi  15261  reeflog  15277  relogef  15278  logrpap0b  15290  loggt0b  15305  1cxp  15314  ecxp  15315  2logb9irrap  15391  0sgm  15399  lgsval2lem  15429  m1lgs  15504  1vgrex  15559  djucllem  15669  bdrabexg  15775  bdunexb  15789  peano5set  15809  speano5  15813  bj-omtrans  15825  pwf1oexmid  15869  nninfsellemeq  15884  iswomninnlem  15921