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  1335  mp3an12  1338  mp3an13  1339  ax9o  1712  sbnfc2  3145  ssdifss  3294  undifss  3532  uneqdifeqim  3537  elssuni  3868  csbexa  4163  difexg  4175  rabexg  4177  abssexg  4216  snexg  4218  copsexg  4278  sotritric  4360  sotritrieq  4361  trsuc  4458  oneli  4464  unexb  4478  opeluu  4486  rabxfr  4506  reuhyp  4508  ordunisuc2r  4551  reg3exmid  4617  brrelex12i  4706  brrelex1i  4707  brrelex2i  4708  xpss2  4775  opabid2  4798  eliunxp  4806  releldmi  4906  relelrni  4907  dmexg  4931  rnexg  4932  elres  4983  resexg  4987  relbrcnvg  5049  brcodir  5058  sotri  5066  sotri2  5068  sotri3  5069  dfrel2  5121  coi1  5186  fco  5424  fssres  5434  fabexg  5446  fvopab3g  5635  mptrcl  5645  mpteqb  5653  elfvmptrab1  5657  ffvelcdmi  5697  fsn2  5737  dfmptg  5742  fvpr1  5767  fvconst2  5779  mptexg  5788  oprabid  5955  ovprc  5958  caovcl  6079  caovass  6085  caovdi  6104  elmpocl  6119  ofexg  6141  resfunexgALT  6166  fo1stresm  6220  fo2ndresm  6221  1stexg  6226  2ndexg  6227  elopabi  6254  mpoexxg  6269  mpoxopn0yelv  6298  rntpos  6316  smores  6351  tfr0dm  6381  tfrlemibxssdm  6386  tfrexlem  6393  tfr1onlembxssdm  6402  tfrcllembxssdm  6415  rdgruledefgg  6434  rdgruledefg  6435  rdgivallem  6440  rdgexg  6448  frec0g  6456  ordgt0ge1  6494  omfnex  6508  oeiv  6515  nna0r  6537  nnm0r  6538  nnsucsssuc  6551  nn2m  6586  nnaordex  6587  nnawordex  6588  ecdmn0m  6637  ecelqsi  6649  ecidg  6659  ectocl  6662  encv  6806  f1oen  6819  ssdomg  6838  map1  6872  fiprc  6875  xpdom1  6895  fict  6930  isinfinf  6959  ac6sfi  6960  xpfi  6994  en1eqsn  7015  fidcenumlemr  7022  fiss  7044  eqinfti  7087  djueq2  7108  djulclr  7116  djurclr  7117  djulcl  7118  djurcl  7119  djuf1olem  7120  djulclb  7122  inl11  7132  eldju1st  7138  1stinl  7141  2ndinl  7142  1stinr  7143  2ndinr  7144  ctssdccl  7178  isomnimap  7204  ismkvmap  7221  iswomnimap  7233  djucomen  7285  exmidapne  7329  0nnq  7433  mulidnq  7458  archnqq  7486  prarloclemarch2  7488  nqnq0pi  7507  nq0m0r  7525  nq02m  7534  prarloclemlt  7562  prarloclemn  7568  prarloclem5  7569  addnqprllem  7596  addnqprulem  7597  appdivnq  7632  1idprl  7659  1idpru  7660  addextpr  7690  cauappcvgprlemdisj  7720  cauappcvgprlemloc  7721  cauappcvgprlemladdru  7725  cauappcvgprlemladdrl  7726  caucvgprlemnbj  7736  caucvgprlemloc  7744  caucvgprprlemnbj  7762  caucvgprprlemloc  7772  caucvgprprlemaddq  7777  suplocexprlemmu  7787  suplocexprlemru  7788  suplocexprlemloc  7790  suplocexprlemlub  7793  0nsr  7818  ltsosr  7833  recexgt0sr  7842  prsrpos  7854  caucvgsr  7871  mappsrprg  7873  suplocsrlem  7877  mulresr  7907  axcnre  7950  axpre-ltwlin  7952  mullid  8026  0re  8028  axmulgt0  8100  ltnsym2  8119  eqlei  8122  ltnei  8132  muladd11  8161  cnegex  8206  0cnALT  8218  negcl  8228  negneg  8278  mul02  8415  mulm1  8428  lt0neg2  8498  le0neg2  8500  recexre  8607  recexgt0  8609  mulge0  8648  gt0ap0i  8656  recextlem1  8680  recexap  8682  recclapzi  8766  recap0apzi  8767  recidapzi  8768  divassapzi  8791  divmulapzi  8792  divdirapzi  8793  rerecclapzi  8805  ltp1  8873  recgt0i  8935  ltmul1i  8949  ltdiv1i  8950  ltmuldivi  8951  ltmul2i  8952  lemul1i  8953  lemul2i  8954  sup3exmid  8986  nngt1ne1  9027  nnrecre  9029  nn0ge0  9276  nn0addcl  9286  nn0mulcl  9287  zgt0ge1  9386  dfuzi  9438  eluzel2  9608  eluz2b1  9677  uz2m1nn  9681  elnn0dc  9687  elnndc  9688  nn01to3  9693  zq  9702  nnrecq  9721  rpge0  9743  rpreccl  9757  mnflt  9860  pnfnlt  9864  mnfle  9869  xrlelttr  9883  xrltletr  9884  xrletr  9885  xgepnf  9893  xlt0neg2  9916  xle0neg2  9918  xaddpnf2  9924  xaddmnf2  9926  xaddid2  9940  elioomnf  10045  ige3m2fz  10126  fzshftral  10185  ige2m1fz1  10186  1fv  10216  4fvwrd4  10217  rebtwn2zlemstep  10344  qbtwnxr  10349  btwnzge0  10392  zmodid2  10446  q2txmodxeq0  10478  frec2uzrand  10499  frecuzrdgtcl  10506  frecfzennn  10520  nn0ennn  10527  uzennn  10530  0exp  10668  sqgt0api  10719  subsq2  10741  qsqeqor  10744  bernneq  10754  faclbnd  10835  faclbnd2  10836  faclbnd3  10837  hashinfuni  10871  hashxp  10920  iswrdiz  10944  2shfti  10998  reim  11019  imcl  11021  crim  11025  caucvgre  11148  rennim  11169  resqrexlemdecn  11179  qabsor  11242  absimle  11251  sqrtthi  11286  sqrtcli  11287  sqrtgt0i  11288  sqrtmsqi  11289  sqrtsqi  11290  sqsqrti  11291  sqrtge0i  11292  absidi  11293  absnidi  11294  xrmaxiflemlub  11415  serclim0  11472  fsum2d  11602  fsumcnv  11604  fsumconst  11621  modfsummodlem1  11623  fsumabs  11632  binom11  11653  prodf1  11709  prodfclim1  11711  prodsnf  11759  fprod2d  11790  fprodcnv  11792  efzval  11850  eftlub  11857  efsep  11858  ef4p  11861  efgt1  11864  reef11  11866  sinf  11871  cosf  11872  efi4p  11884  sinneg  11893  cosneg  11894  efival  11899  efmival  11900  cos01gt0  11930  sin02gt0  11931  absefib  11938  efieq1re  11939  demoivre  11940  demoivreALT  11941  eirraplem  11944  0dvds  11978  odd2np1lem  12039  odd2np1  12040  even2n  12041  mod2eq0even  12045  2teven  12054  opoe  12062  omoe  12063  opeo  12064  omeo  12065  m1exp1  12068  bits0e  12116  bits0o  12117  bitsinv1  12129  gcd0id  12156  gcdid0  12157  1gcd  12169  lcmdvds  12257  isprm2lem  12294  isprm3  12296  prmgt1  12310  coprm  12322  isevengcd2  12336  isoddgcd1  12337  sqpweven  12353  2sqpwodd  12354  pythagtriplem12  12454  pythagtriplem13  12455  pythagtriplem14  12456  pythagtriplem16  12458  pc2dvds  12509  oddprmdvds  12533  pockthi  12537  1arith2  12547  unennn  12624  ctinfomlemom  12654  qnnen  12658  ssnnctlemct  12673  strslfv  12733  strle1g  12794  1strbas  12805  tgval  12943  ismgmn0  13011  mulgval  13262  mulgfng  13264  mulg0  13265  mulg1  13269  mulg2  13271  isnsg  13342  ringidvalg  13527  issrg  13531  subrgpropd  13819  rrgval  13828  islmod  13857  scaffvalg  13872  islssm  13923  sraval  14003  mopnset  14118  metuex  14121  zrhval  14183  zrhvalg  14184  zrhex  14187  psrbag  14233  istopon  14259  eltg4i  14301  eltg3  14303  tg1  14305  tg2  14306  topnex  14332  cldrcl  14348  restsn  14426  lmrcl  14437  metflem  14595  xmetf  14596  ismet2  14600  xmeteq0  14605  xmettri2  14607  xmetpsmet  14615  xmetres2  14625  blfvalps  14631  blex  14633  blvalps  14634  blval  14635  blfps  14655  blf  14656  mopnval  14688  cnbl0  14780  cnblcld  14781  blssioo  14799  resubmet  14802  cncfmet  14838  cnplimcim  14913  cnlimcim  14917  cnlimc  14918  dvfgg  14934  dvfpm  14935  dvfcnpm  14936  dvcj  14955  dvmptfsum  14971  reeff1olem  15017  ef2kpi  15052  sinperlem  15054  sin2kpi  15057  cos2kpi  15058  sinhalfpip  15066  sinhalfpim  15067  coshalfpip  15068  coshalfpim  15069  sincosq1sgn  15072  sinq12gt0  15076  sinkpi  15093  reeflog  15109  relogef  15110  logrpap0b  15122  loggt0b  15137  1cxp  15146  ecxp  15147  2logb9irrap  15223  0sgm  15231  lgsval2lem  15261  m1lgs  15336  djucllem  15456  bdrabexg  15562  bdunexb  15576  peano5set  15596  speano5  15600  bj-omtrans  15612  pwf1oexmid  15654  nninfsellemeq  15668  iswomninnlem  15703