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  s1leng  11076  s1fv  11078  s111  11083  2shfti  11113  reim  11134  imcl  11136  crim  11140  caucvgre  11263  rennim  11284  resqrexlemdecn  11294  qabsor  11357  absimle  11366  sqrtthi  11401  sqrtcli  11402  sqrtgt0i  11403  sqrtmsqi  11404  sqrtsqi  11405  sqsqrti  11406  sqrtge0i  11407  absidi  11408  absnidi  11409  xrmaxiflemlub  11530  serclim0  11587  fsum2d  11717  fsumcnv  11719  fsumconst  11736  modfsummodlem1  11738  fsumabs  11747  binom11  11768  prodf1  11824  prodfclim1  11826  prodsnf  11874  fprod2d  11905  fprodcnv  11907  efzval  11965  eftlub  11972  efsep  11973  ef4p  11976  efgt1  11979  reef11  11981  sinf  11986  cosf  11987  efi4p  11999  sinneg  12008  cosneg  12009  efival  12014  efmival  12015  cos01gt0  12045  sin02gt0  12046  absefib  12053  efieq1re  12054  demoivre  12055  demoivreALT  12056  eirraplem  12059  0dvds  12093  odd2np1lem  12154  odd2np1  12155  even2n  12156  mod2eq0even  12160  2teven  12169  opoe  12177  omoe  12178  opeo  12179  omeo  12180  m1exp1  12183  bits0e  12231  bits0o  12232  bitsinv1  12244  gcd0id  12271  gcdid0  12272  1gcd  12284  lcmdvds  12372  isprm2lem  12409  isprm3  12411  prmgt1  12425  coprm  12437  isevengcd2  12451  isoddgcd1  12452  sqpweven  12468  2sqpwodd  12469  pythagtriplem12  12569  pythagtriplem13  12570  pythagtriplem14  12571  pythagtriplem16  12573  pc2dvds  12624  oddprmdvds  12648  pockthi  12652  1arith2  12662  unennn  12739  ctinfomlemom  12769  qnnen  12773  ssnnctlemct  12788  strslfv  12848  strle1g  12909  1strbas  12920  tgval  13065  ismgmn0  13161  mulgval  13429  mulgfng  13431  mulg0  13432  mulg1  13436  mulg2  13438  isnsg  13509  ringidvalg  13694  issrg  13698  subrgpropd  13986  rrgval  13995  islmod  14024  scaffvalg  14039  islssm  14090  sraval  14170  mopnset  14285  metuex  14288  zrhval  14350  zrhvalg  14351  zrhex  14354  psrbag  14402  istopon  14456  eltg4i  14498  eltg3  14500  tg1  14502  tg2  14503  topnex  14529  cldrcl  14545  restsn  14623  lmrcl  14634  metflem  14792  xmetf  14793  ismet2  14797  xmeteq0  14802  xmettri2  14804  xmetpsmet  14812  xmetres2  14822  blfvalps  14828  blex  14830  blvalps  14831  blval  14832  blfps  14852  blf  14853  mopnval  14885  cnbl0  14977  cnblcld  14978  blssioo  14996  resubmet  14999  cncfmet  15035  cnplimcim  15110  cnlimcim  15114  cnlimc  15115  dvfgg  15131  dvfpm  15132  dvfcnpm  15133  dvcj  15152  dvmptfsum  15168  reeff1olem  15214  ef2kpi  15249  sinperlem  15251  sin2kpi  15254  cos2kpi  15255  sinhalfpip  15263  sinhalfpim  15264  coshalfpip  15265  coshalfpim  15266  sincosq1sgn  15269  sinq12gt0  15273  sinkpi  15290  reeflog  15306  relogef  15307  logrpap0b  15319  loggt0b  15334  1cxp  15343  ecxp  15344  2logb9irrap  15420  0sgm  15428  lgsval2lem  15458  m1lgs  15533  1vgrex  15588  djucllem  15698  bdrabexg  15804  bdunexb  15818  peano5set  15838  speano5  15842  bj-omtrans  15854  pwf1oexmid  15898  nninfsellemeq  15913  iswomninnlem  15950