Theorem mpan 421

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 419	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  423  mpanl12  433  mp3an1  1314  mp3an12  1317  mp3an13  1318  ax9o  1686  sbnfc2  3104  ssdifss  3251  undifss  3488  uneqdifeqim  3493  elssuni  3816  csbexa  4110  difexg  4122  rabexg  4124  abssexg  4160  snexg  4162  copsexg  4221  sotritric  4301  sotritrieq  4302  trsuc  4399  oneli  4405  unexb  4419  opeluu  4427  rabxfr  4447  reuhyp  4449  ordunisuc2r  4490  reg3exmid  4556  brrelex12i  4645  brrelex1i  4646  brrelex2i  4647  xpss2  4714  opabid2  4734  eliunxp  4742  releldmi  4842  relelrni  4843  dmexg  4867  rnexg  4868  elres  4919  resexg  4923  relbrcnvg  4982  brcodir  4990  sotri  4998  sotri2  5000  sotri3  5001  dfrel2  5053  coi1  5118  fco  5352  fssres  5362  fabexg  5374  fvopab3g  5558  mptrcl  5567  mpteqb  5575  elfvmptrab1  5579  ffvelrni  5618  fsn2  5658  dfmptg  5663  fvpr1  5688  fvconst2  5700  mptexg  5709  oprabid  5870  ovprc  5873  caovcl  5992  caovass  5998  caovdi  6017  elmpocl  6035  ofexg  6053  resfunexgALT  6075  fo1stresm  6126  fo2ndresm  6127  1stexg  6132  2ndexg  6133  elopabi  6160  mpoexxg  6175  mpoxopn0yelv  6203  rntpos  6221  smores  6256  tfr0dm  6286  tfrlemibxssdm  6291  tfrexlem  6298  tfr1onlembxssdm  6307  tfrcllembxssdm  6320  rdgruledefgg  6339  rdgruledefg  6340  rdgivallem  6345  rdgexg  6353  frec0g  6361  ordgt0ge1  6399  omfnex  6413  oeiv  6420  nna0r  6442  nnm0r  6443  nnsucsssuc  6456  nn2m  6490  nnaordex  6491  nnawordex  6492  ecdmn0m  6539  ecelqsi  6551  ecidg  6561  ectocl  6564  encv  6708  f1oen  6721  ssdomg  6740  map1  6774  fiprc  6777  xpdom1  6797  fict  6830  isinfinf  6859  ac6sfi  6860  xpfi  6891  en1eqsn  6909  fidcenumlemr  6916  fiss  6938  eqinfti  6981  djueq2  7002  djulclr  7010  djurclr  7011  djulcl  7012  djurcl  7013  djuf1olem  7014  djulclb  7016  inl11  7026  eldju1st  7032  1stinl  7035  2ndinl  7036  1stinr  7037  2ndinr  7038  ctssdccl  7072  isomnimap  7097  ismkvmap  7114  iswomnimap  7126  djucomen  7168  0nnq  7301  mulidnq  7326  archnqq  7354  prarloclemarch2  7356  nqnq0pi  7375  nq0m0r  7393  nq02m  7402  prarloclemlt  7430  prarloclemn  7436  prarloclem5  7437  addnqprllem  7464  addnqprulem  7465  appdivnq  7500  1idprl  7527  1idpru  7528  addextpr  7558  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  caucvgprlemnbj  7604  caucvgprlemloc  7612  caucvgprprlemnbj  7630  caucvgprprlemloc  7640  caucvgprprlemaddq  7645  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemloc  7658  suplocexprlemlub  7661  0nsr  7686  ltsosr  7701  recexgt0sr  7710  prsrpos  7722  caucvgsr  7739  mappsrprg  7741  suplocsrlem  7745  mulresr  7775  axcnre  7818  axpre-ltwlin  7820  mulid2  7893  0re  7895  axmulgt0  7966  ltnsym2  7985  eqlei  7988  ltnei  7998  muladd11  8027  cnegex  8072  0cnALT  8084  negcl  8094  negneg  8144  mul02  8281  mulm1  8294  lt0neg2  8363  le0neg2  8365  recexre  8472  recexgt0  8474  mulge0  8513  gt0ap0i  8521  recextlem1  8544  recexap  8546  recclapzi  8629  recap0apzi  8630  recidapzi  8631  divassapzi  8654  divmulapzi  8655  divdirapzi  8656  rerecclapzi  8668  ltp1  8735  recgt0i  8797  ltmul1i  8811  ltdiv1i  8812  ltmuldivi  8813  ltmul2i  8814  lemul1i  8815  lemul2i  8816  sup3exmid  8848  nngt1ne1  8888  nnrecre  8890  nn0ge0  9135  nn0addcl  9145  nn0mulcl  9146  zgt0ge1  9245  dfuzi  9297  eluzel2  9467  eluz2b1  9535  uz2m1nn  9539  elnn0dc  9545  elnndc  9546  nn01to3  9551  zq  9560  nnrecq  9579  rpge0  9598  rpreccl  9612  mnflt  9715  pnfnlt  9719  mnfle  9724  xrlelttr  9738  xrltletr  9739  xrletr  9740  xgepnf  9748  xlt0neg2  9771  xle0neg2  9773  xaddpnf2  9779  xaddmnf2  9781  xaddid2  9795  elioomnf  9900  ige3m2fz  9980  fzshftral  10039  ige2m1fz1  10040  1fv  10070  4fvwrd4  10071  rebtwn2zlemstep  10184  qbtwnxr  10189  btwnzge0  10231  zmodid2  10283  q2txmodxeq0  10315  frec2uzrand  10336  frecuzrdgtcl  10343  frecfzennn  10357  nn0ennn  10364  uzennn  10367  0exp  10486  sqgt0api  10536  subsq2  10558  qsqeqor  10561  bernneq  10571  faclbnd  10650  faclbnd2  10651  faclbnd3  10652  hashinfuni  10686  hashxp  10735  2shfti  10769  reim  10790  imcl  10792  crim  10796  caucvgre  10919  rennim  10940  resqrexlemdecn  10950  qabsor  11013  absimle  11022  sqrtthi  11057  sqrtcli  11058  sqrtgt0i  11059  sqrtmsqi  11060  sqrtsqi  11061  sqsqrti  11062  sqrtge0i  11063  absidi  11064  absnidi  11065  xrmaxiflemlub  11185  serclim0  11242  fsum2d  11372  fsumcnv  11374  fsumconst  11391  modfsummodlem1  11393  fsumabs  11402  binom11  11423  prodf1  11479  prodfclim1  11481  prodsnf  11529  fprod2d  11560  fprodcnv  11562  efzval  11620  eftlub  11627  efsep  11628  ef4p  11631  efgt1  11634  reef11  11636  sinf  11641  cosf  11642  efi4p  11654  sinneg  11663  cosneg  11664  efival  11669  efmival  11670  cos01gt0  11699  sin02gt0  11700  absefib  11707  efieq1re  11708  demoivre  11709  demoivreALT  11710  eirraplem  11713  0dvds  11747  odd2np1lem  11805  odd2np1  11806  even2n  11807  mod2eq0even  11811  2teven  11820  opoe  11828  omoe  11829  opeo  11830  omeo  11831  m1exp1  11834  gcd0id  11908  gcdid0  11909  1gcd  11921  lcmdvds  12007  isprm2lem  12044  isprm3  12046  prmgt1  12060  coprm  12072  isevengcd2  12086  isoddgcd1  12087  sqpweven  12103  2sqpwodd  12104  pythagtriplem12  12203  pythagtriplem13  12204  pythagtriplem14  12205  pythagtriplem16  12207  pc2dvds  12257  oddprmdvds  12280  pockthi  12284  1arith2  12294  unennn  12326  ctinfomlemom  12356  qnnen  12360  ssnnctlemct  12375  strslfv  12434  strle1g  12480  1strbas  12489  istopon  12611  tgval  12649  eltg4i  12655  eltg3  12657  tg1  12659  tg2  12660  topnex  12686  cldrcl  12702  restsn  12780  lmrcl  12791  metflem  12949  xmetf  12950  ismet2  12954  xmeteq0  12959  xmettri2  12961  xmetpsmet  12969  xmetres2  12979  blfvalps  12985  blex  12987  blvalps  12988  blval  12989  blfps  13009  blf  13010  mopnval  13042  cnbl0  13134  cnblcld  13135  blssioo  13145  resubmet  13148  cncfmet  13179  cnplimcim  13236  cnlimcim  13240  cnlimc  13241  dvfgg  13257  dvfpm  13258  dvfcnpm  13259  dvcj  13273  reeff1olem  13292  ef2kpi  13327  sinperlem  13329  sin2kpi  13332  cos2kpi  13333  sinhalfpip  13341  sinhalfpim  13342  coshalfpip  13343  coshalfpim  13344  sincosq1sgn  13347  sinq12gt0  13351  sinkpi  13368  reeflog  13384  relogef  13385  logrpap0b  13397  loggt0b  13412  1cxp  13421  ecxp  13422  2logb9irrap  13495  lgsval2lem  13511  djucllem  13641  bdrabexg  13748  bdunexb  13762  peano5set  13782  speano5  13786  bj-omtrans  13798  pwf1oexmid  13839  nninfsellemeq  13854  iswomninnlem  13888