Theorem mpan 422

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 420	1 |- ( ps -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mp2an  424  mpanl12  434  mp3an1  1319  mp3an12  1322  mp3an13  1323  ax9o  1691  sbnfc2  3109  ssdifss  3257  undifss  3495  uneqdifeqim  3500  elssuni  3824  csbexa  4118  difexg  4130  rabexg  4132  abssexg  4168  snexg  4170  copsexg  4229  sotritric  4309  sotritrieq  4310  trsuc  4407  oneli  4413  unexb  4427  opeluu  4435  rabxfr  4455  reuhyp  4457  ordunisuc2r  4498  reg3exmid  4564  brrelex12i  4653  brrelex1i  4654  brrelex2i  4655  xpss2  4722  opabid2  4742  eliunxp  4750  releldmi  4850  relelrni  4851  dmexg  4875  rnexg  4876  elres  4927  resexg  4931  relbrcnvg  4990  brcodir  4998  sotri  5006  sotri2  5008  sotri3  5009  dfrel2  5061  coi1  5126  fco  5363  fssres  5373  fabexg  5385  fvopab3g  5569  mptrcl  5578  mpteqb  5586  elfvmptrab1  5590  ffvelrni  5630  fsn2  5670  dfmptg  5675  fvpr1  5700  fvconst2  5712  mptexg  5721  oprabid  5885  ovprc  5888  caovcl  6007  caovass  6013  caovdi  6032  elmpocl  6047  ofexg  6065  resfunexgALT  6087  fo1stresm  6140  fo2ndresm  6141  1stexg  6146  2ndexg  6147  elopabi  6174  mpoexxg  6189  mpoxopn0yelv  6218  rntpos  6236  smores  6271  tfr0dm  6301  tfrlemibxssdm  6306  tfrexlem  6313  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  rdgruledefgg  6354  rdgruledefg  6355  rdgivallem  6360  rdgexg  6368  frec0g  6376  ordgt0ge1  6414  omfnex  6428  oeiv  6435  nna0r  6457  nnm0r  6458  nnsucsssuc  6471  nn2m  6506  nnaordex  6507  nnawordex  6508  ecdmn0m  6555  ecelqsi  6567  ecidg  6577  ectocl  6580  encv  6724  f1oen  6737  ssdomg  6756  map1  6790  fiprc  6793  xpdom1  6813  fict  6846  isinfinf  6875  ac6sfi  6876  xpfi  6907  en1eqsn  6925  fidcenumlemr  6932  fiss  6954  eqinfti  6997  djueq2  7018  djulclr  7026  djurclr  7027  djulcl  7028  djurcl  7029  djuf1olem  7030  djulclb  7032  inl11  7042  eldju1st  7048  1stinl  7051  2ndinl  7052  1stinr  7053  2ndinr  7054  ctssdccl  7088  isomnimap  7113  ismkvmap  7130  iswomnimap  7142  djucomen  7193  0nnq  7326  mulidnq  7351  archnqq  7379  prarloclemarch2  7381  nqnq0pi  7400  nq0m0r  7418  nq02m  7427  prarloclemlt  7455  prarloclemn  7461  prarloclem5  7462  addnqprllem  7489  addnqprulem  7490  appdivnq  7525  1idprl  7552  1idpru  7553  addextpr  7583  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemnbj  7629  caucvgprlemloc  7637  caucvgprprlemnbj  7655  caucvgprprlemloc  7665  caucvgprprlemaddq  7670  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemloc  7683  suplocexprlemlub  7686  0nsr  7711  ltsosr  7726  recexgt0sr  7735  prsrpos  7747  caucvgsr  7764  mappsrprg  7766  suplocsrlem  7770  mulresr  7800  axcnre  7843  axpre-ltwlin  7845  mulid2  7918  0re  7920  axmulgt0  7991  ltnsym2  8010  eqlei  8013  ltnei  8023  muladd11  8052  cnegex  8097  0cnALT  8109  negcl  8119  negneg  8169  mul02  8306  mulm1  8319  lt0neg2  8388  le0neg2  8390  recexre  8497  recexgt0  8499  mulge0  8538  gt0ap0i  8546  recextlem1  8569  recexap  8571  recclapzi  8654  recap0apzi  8655  recidapzi  8656  divassapzi  8679  divmulapzi  8680  divdirapzi  8681  rerecclapzi  8693  ltp1  8760  recgt0i  8822  ltmul1i  8836  ltdiv1i  8837  ltmuldivi  8838  ltmul2i  8839  lemul1i  8840  lemul2i  8841  sup3exmid  8873  nngt1ne1  8913  nnrecre  8915  nn0ge0  9160  nn0addcl  9170  nn0mulcl  9171  zgt0ge1  9270  dfuzi  9322  eluzel2  9492  eluz2b1  9560  uz2m1nn  9564  elnn0dc  9570  elnndc  9571  nn01to3  9576  zq  9585  nnrecq  9604  rpge0  9623  rpreccl  9637  mnflt  9740  pnfnlt  9744  mnfle  9749  xrlelttr  9763  xrltletr  9764  xrletr  9765  xgepnf  9773  xlt0neg2  9796  xle0neg2  9798  xaddpnf2  9804  xaddmnf2  9806  xaddid2  9820  elioomnf  9925  ige3m2fz  10005  fzshftral  10064  ige2m1fz1  10065  1fv  10095  4fvwrd4  10096  rebtwn2zlemstep  10209  qbtwnxr  10214  btwnzge0  10256  zmodid2  10308  q2txmodxeq0  10340  frec2uzrand  10361  frecuzrdgtcl  10368  frecfzennn  10382  nn0ennn  10389  uzennn  10392  0exp  10511  sqgt0api  10561  subsq2  10583  qsqeqor  10586  bernneq  10596  faclbnd  10675  faclbnd2  10676  faclbnd3  10677  hashinfuni  10711  hashxp  10761  2shfti  10795  reim  10816  imcl  10818  crim  10822  caucvgre  10945  rennim  10966  resqrexlemdecn  10976  qabsor  11039  absimle  11048  sqrtthi  11083  sqrtcli  11084  sqrtgt0i  11085  sqrtmsqi  11086  sqrtsqi  11087  sqsqrti  11088  sqrtge0i  11089  absidi  11090  absnidi  11091  xrmaxiflemlub  11211  serclim0  11268  fsum2d  11398  fsumcnv  11400  fsumconst  11417  modfsummodlem1  11419  fsumabs  11428  binom11  11449  prodf1  11505  prodfclim1  11507  prodsnf  11555  fprod2d  11586  fprodcnv  11588  efzval  11646  eftlub  11653  efsep  11654  ef4p  11657  efgt1  11660  reef11  11662  sinf  11667  cosf  11668  efi4p  11680  sinneg  11689  cosneg  11690  efival  11695  efmival  11696  cos01gt0  11725  sin02gt0  11726  absefib  11733  efieq1re  11734  demoivre  11735  demoivreALT  11736  eirraplem  11739  0dvds  11773  odd2np1lem  11831  odd2np1  11832  even2n  11833  mod2eq0even  11837  2teven  11846  opoe  11854  omoe  11855  opeo  11856  omeo  11857  m1exp1  11860  gcd0id  11934  gcdid0  11935  1gcd  11947  lcmdvds  12033  isprm2lem  12070  isprm3  12072  prmgt1  12086  coprm  12098  isevengcd2  12112  isoddgcd1  12113  sqpweven  12129  2sqpwodd  12130  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem14  12231  pythagtriplem16  12233  pc2dvds  12283  oddprmdvds  12306  pockthi  12310  1arith2  12320  unennn  12352  ctinfomlemom  12382  qnnen  12386  ssnnctlemct  12401  strslfv  12460  strle1g  12508  1strbas  12517  ismgmn0  12612  istopon  12805  tgval  12843  eltg4i  12849  eltg3  12851  tg1  12853  tg2  12854  topnex  12880  cldrcl  12896  restsn  12974  lmrcl  12985  metflem  13143  xmetf  13144  ismet2  13148  xmeteq0  13153  xmettri2  13155  xmetpsmet  13163  xmetres2  13173  blfvalps  13179  blex  13181  blvalps  13182  blval  13183  blfps  13203  blf  13204  mopnval  13236  cnbl0  13328  cnblcld  13329  blssioo  13339  resubmet  13342  cncfmet  13373  cnplimcim  13430  cnlimcim  13434  cnlimc  13435  dvfgg  13451  dvfpm  13452  dvfcnpm  13453  dvcj  13467  reeff1olem  13486  ef2kpi  13521  sinperlem  13523  sin2kpi  13526  cos2kpi  13527  sinhalfpip  13535  sinhalfpim  13536  coshalfpip  13537  coshalfpim  13538  sincosq1sgn  13541  sinq12gt0  13545  sinkpi  13562  reeflog  13578  relogef  13579  logrpap0b  13591  loggt0b  13606  1cxp  13615  ecxp  13616  2logb9irrap  13689  lgsval2lem  13705  djucllem  13835  bdrabexg  13941  bdunexb  13955  peano5set  13975  speano5  13979  bj-omtrans  13991  pwf1oexmid  14032  nninfsellemeq  14047  iswomninnlem  14081