Theorem mpan 428

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mp2an  430  mpanl12  440  mp3an1  1365  mp3an12  1368  mp3an13  1369  ax9o  1750  sbnfc2  3208  ssdifss  3359  undifss  3608  uneqdifeqim  3613  elssuni  3963  csbexa  4262  difexg  4275  rabexg  4279  abssexg  4319  snexg  4321  copsexg  4384  sotritric  4469  sotritrieq  4470  trsuc  4567  oneli  4573  unexb  4588  opeluu  4596  rabxfr  4616  reuhyp  4618  ordunisuc2r  4661  reg3exmid  4727  brrelex12i  4817  brrelex1i  4818  brrelex2i  4819  xpss2  4886  opabid2  4911  eliunxp  4919  releldmi  5021  relelrni  5022  dmexg  5046  rnexg  5047  elres  5099  resexg  5103  relbrcnvg  5166  brcodir  5175  sotri  5183  sotri2  5185  sotri3  5186  dfrel2  5238  coi1  5303  fco  5552  fssres  5565  fabexg  5579  fvopab3g  5778  mptrcl  5788  mpteqb  5796  elfvmptrab1  5801  fvopab4ndm  5803  ffvelcdmi  5842  fsn2  5882  dfmptg  5888  fcof  5894  fvpr1  5919  fvconst2  5931  mptexg  5942  oprabid  6117  ovprc  6121  caovcl  6244  caovass  6250  caovdi  6269  elmpocl  6284  relmptopab  6291  ofexg  6307  resfunexgALT  6337  fo1stresm  6395  fo2ndresm  6396  1stexg  6401  2ndexg  6402  elopabi  6431  mpoexxg  6446  elmpom  6474  supp0  6478  mpoxopn0yelv  6510  rntpos  6528  smores  6563  tfr0dm  6593  tfrlemibxssdm  6598  tfrexlem  6605  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  rdgruledefgg  6646  rdgruledefg  6647  rdgivallem  6652  rdgexg  6660  frec0g  6668  ordgt0ge1  6708  omfnex  6722  oeiv  6729  nna0r  6751  nnm0r  6752  nnsucsssuc  6765  nn2m  6800  nnaordex  6801  nnawordex  6802  ecdmn0m  6851  ecelqsi  6863  ecidg  6873  ectocl  6876  mapfset  6945  encv  7028  f1oen  7045  ssdomg  7065  map1  7101  fiprc  7104  dom1o  7116  xpdom1  7133  fict  7170  isinfinf  7201  ac6sfi  7202  xpfi  7239  en1eqsn  7265  fidcenumlemr  7272  fiss  7311  fipwfi  7321  eqinfti  7360  djueq2  7381  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  djuf1olem  7393  djulclb  7395  inl11  7405  eldju1st  7411  1stinl  7414  2ndinl  7415  1stinr  7416  2ndinr  7417  ctssdccl  7451  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  finacn  7560  djucomen  7572  exmidapne  7626  0nnq  7731  mulidnq  7756  archnqq  7784  prarloclemarch2  7786  nqnq0pi  7805  nq0m0r  7823  nq02m  7832  prarloclemlt  7860  prarloclemn  7866  prarloclem5  7867  addnqprllem  7894  addnqprulem  7895  appdivnq  7930  1idprl  7957  1idpru  7958  addextpr  7988  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemnbj  8034  caucvgprlemloc  8042  caucvgprprlemnbj  8060  caucvgprprlemloc  8070  caucvgprprlemaddq  8075  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemloc  8088  suplocexprlemlub  8091  0nsr  8116  ltsosr  8131  recexgt0sr  8140  prsrpos  8152  caucvgsr  8169  mappsrprg  8171  suplocsrlem  8175  mulresr  8205  axcnre  8248  axpre-ltwlin  8250  mullid  8324  0re  8326  axmulgt0  8397  ltnsym2  8416  eqlei  8420  ltnei  8430  muladd11  8460  cnegex  8505  0cnALT  8517  negcl  8527  negneg  8577  mul02  8715  mulm1  8728  lt0neg2  8798  le0neg2  8800  recexre  8908  recexgt0  8910  mulge0  8949  gt0ap0i  8957  recextlem1  8981  recexap  8983  recclapzi  9069  recap0apzi  9070  recidapzi  9071  divassapzi  9094  divmulapzi  9095  divdirapzi  9096  rerecclapzi  9108  ltp1  9176  recgt0i  9238  ltmul1i  9252  ltdiv1i  9253  ltmuldivi  9254  ltmul2i  9255  lemul1i  9256  lemul2i  9257  sup3exmid  9289  nngt1ne1  9341  nnrecre  9343  nn0ge0  9592  nn0addcl  9602  nn0mulcl  9603  zgt0ge1  9707  dfuzi  9760  eluzel2  9935  eluz2b1  10010  uz2m1nn  10014  elnn0dc  10020  elnndc  10021  nn01to3  10026  zq  10035  nnrecq  10054  rpge0  10077  rpreccl  10091  mnflt  10195  pnfnlt  10199  mnfle  10204  xrlelttr  10218  xrltletr  10219  xrletr  10220  xgepnf  10228  xlt0neg2  10251  xle0neg2  10253  xaddpnf2  10259  xaddmnf2  10261  xaddid2  10275  elioomnf  10380  ige3m2fz  10464  fzshftral  10525  ige2m1fz1  10526  1fv  10556  4fvwrd4  10557  rebtwn2zlemstep  10697  qbtwnxr  10702  btwnzge0  10748  zmodid2  10802  q2txmodxeq0  10834  frec2uzrand  10855  frecuzrdgtcl  10862  frecfzennn  10876  nn0ennn  10883  uzennn  10886  0exp  11024  sqgt0api  11075  subsq2  11097  qsqeqor  11100  bernneq  11111  faclbnd  11193  faclbnd2  11194  faclbnd3  11195  hashinfuni  11230  hashxp  11281  hashpwfi  11283  iswrdiz  11325  lsw0  11366  ccatlid  11388  s1leng  11406  s1fv  11408  s111  11413  pfx0g  11462  2shfti  11610  reim  11631  imcl  11633  crim  11637  caucvgre  11761  rennim  11782  resqrexlemdecn  11792  qabsor  11855  absimle  11865  sqrtthi  11900  sqrtcli  11901  sqrtgt0i  11902  sqrtmsqi  11903  sqrtsqi  11904  sqsqrti  11905  sqrtge0i  11906  absidi  11907  absnidi  11908  xrmaxiflemlub  12030  serclim0  12087  fsum2d  12218  fsumcnv  12220  fsumconst  12237  modfsummodlem1  12239  fsumabs  12248  binom11  12269  prodf1  12325  prodfclim1  12327  prodsnf  12375  fprod2d  12406  fprodcnv  12408  efzval  12466  eftlub  12473  efsep  12474  ef4p  12477  efgt1  12480  reef11  12482  sinf  12487  cosf  12488  efi4p  12500  sinneg  12509  cosneg  12510  efival  12515  efmival  12516  cos01gt0  12546  sin02gt0  12547  absefib  12554  efieq1re  12555  demoivre  12556  demoivreALT  12557  eirraplem  12560  0dvds  12594  odd2np1lem  12655  odd2np1  12656  even2n  12657  mod2eq0even  12661  2teven  12670  opoe  12678  omoe  12679  opeo  12680  omeo  12681  m1exp1  12684  bits0e  12732  bits0o  12733  bitsinv1  12745  gcd0id  12772  gcdid0  12773  1gcd  12785  lcmdvds  12873  isprm2lem  12910  isprm3  12912  prmgt1  12927  coprm  12939  isevengcd2  12953  isoddgcd1  12954  sqpweven  12971  2sqpwodd  12972  sqrtrirr  13005  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem14  13076  pythagtriplem16  13078  pc2dvds  13129  oddprmdvds  13153  pockthi  13157  1arith2  13167  prmlem1a  13241  unennn  13337  ctinfomlemom  13367  qnnen  13371  ssnnctlemct  13386  strslfv  13446  slotm  13464  strle1g  13509  1strbas  13520  tgval  13665  ismgmn0  13727  mulgval  13974  mulgfng  13976  mulg0  13977  mulg1  13981  mulg2  13983  isnsg  14054  mgpplusg  14271  mgpbas  14274  ringidvalg  14313  ringidval  14314  issrg  14318  subrgpropd  14610  rrgval  14619  islmod  14676  scaffvalg  14692  islssm  14743  sraval  14823  mopnset  14938  metuex  14941  zrhval  15001  zrhvalg  15002  zrhex  15005  asclfval  15070  psrbag  15102  psrbagaddclfi  15110  istopon  15163  eltg4i  15205  eltg3  15207  tg1  15209  tg2  15210  topnex  15236  cldrcl  15252  restsn  15330  lmrcl  15342  metflem  15499  xmetf  15500  ismet2  15504  xmeteq0  15509  xmettri2  15511  xmetpsmet  15519  xmetres2  15529  blfvalps  15535  blex  15537  blvalps  15538  blval  15539  blfps  15559  blf  15560  mopnval  15592  cnbl0  15684  cnblcld  15685  blssioo  15703  resubmet  15706  cncfmet  15742  cnplimcim  15817  cnlimcim  15821  cnlimc  15822  dvfgg  15838  dvfpm  15839  dvfcnpm  15840  dvcj  15859  dvmptfsum  15875  reeff1olem  15921  ef2kpi  15957  sinperlem  15959  sin2kpi  15962  cos2kpi  15963  sinhalfpip  15971  sinhalfpim  15972  coshalfpip  15973  coshalfpim  15974  sincosq1sgn  15977  sinq12gt0  15981  sinkpi  15998  reeflog  16014  relogef  16015  logrpap0b  16028  loggt0b  16043  1cxp  16055  ecxp  16056  2logb9irrap  16132  log2tlbndlog2  16139  log2ublem2  16141  0sgm  16166  pcbcctr  16201  bcp1ctr  16204  bclbnd  16205  bposlem1  16209  lgsval2lem  16227  m1lgs  16302  1vgrex  16359  upgrfi  16441  umgredgnlp  16491  wlkop  16687  clwwlkn0  16747  djucllem  16926  bdrabexg  17030  bdunexb  17044  peano5set  17064  speano5  17068  bj-omtrans  17080  pw1ninf  17119  pwf1oexmid  17127  nninfsellemeq  17155  iswomninnlem  17197