Theorem mpan2 401

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2.1	|- ps
mpan2.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpan2	|- ( ph -> ch )

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		mpan2.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpdan 398	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 97

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

This theorem is referenced by:  mpanr12  415  mp3an23  1224  equs4  1613  sb4bor  1716  eueq2dc  2714  sbcgf  2825  csbconstgf  2863  sbcnestg  2899  csbnestg  2900  csbnest1g  2901  ssindif0im  3281  mpteq1  3841  iinexgm  3908  mss  3962  eusv2nf  4188  eldifpw  4208  ordtriexmid  4247  onsucsssucexmid  4252  ordsucunielexmid  4256  nn0suc  4327  xpss1  4448  xpiindim  4473  reldm0  4553  elrnmpt1s  4584  resdm  4649  resid  4662  eliniseg  4695  trinxp  4718  inimasn  4741  ssrnres  4763  cnveq0  4777  coi2  4837  relrelss  4844  funcnvres  4972  funimaex  4984  fnresin1  5013  fnresin2  5014  fresin  5068  dffv3g  5174  ssimaex  5234  dmfco  5241  fvmpt  5249  fsn  5335  fsn2  5337  elabrex  5397  f1elima  5412  2ndconst  5843  tposfun  5875  tpostpos2  5880  tfrexlem  5948  tfri3  5953  rdgruledefgg  5962  rdgss  5970  frecsuclem3  5990  frecrdg  5992  oa0  6037  om0  6038  oei0  6039  oav2  6043  oa1suc  6047  nnmsucr  6067  nnm1  6097  nnm2  6098  ecelqsg  6159  ecidg  6170  xpiderm  6177  qsel  6183  xp1en  6297  xpcomco  6300  findcard2s  6347  findcard2d  6348  findcard2sd  6349  mulidpi  6416  nlt1pig  6439  indpi  6440  halfnqq  6508  archnqq  6515  prarloclemarch  6516  prarloclemarch2  6517  nnnq  6520  nq0a0  6555  addpinq1  6562  prarloclemlt  6591  prarloclemlo  6592  prarloclem3  6595  prarloclemcalc  6600  nqprm  6640  addnqpr1  6660  1idprl  6688  1idpru  6689  1idpr  6690  recexprlem1ssl  6731  recexprlem1ssu  6732  ltmprr  6740  0idsr  6852  1idsr  6853  00sr  6854  pn0sr  6856  negexsr  6857  recexgt0sr  6858  archsr  6866  prsrcl  6868  prsradd  6870  elrealeu  6906  pitonnlem1p1  6922  peano2nnnn  6929  ax1rid  6951  axcnre  6955  peano5nnnn  6966  peano2cn  7148  peano2re  7149  addid2  7152  subid  7230  subid1  7231  negid  7258  negeq0  7265  peano2cnm  7277  peano2rem  7278  mul01  7386  lt0neg1  7463  le0neg1  7465  recexre  7569  inelr  7575  rimul  7576  reapmul1  7586  apsqgt0  7592  mulge0  7610  negap0  7620  divvalap  7653  rerecclap  7706  div2negap  7711  divgt0i2i  7883  peano5nni  7917  nnge1  7937  times2  8039  addltmul  8161  nn0p1nn  8221  peano2nn0  8222  nn0lele2xi  8233  znnnlt1  8293  nn0lt10b  8321  prime  8337  msqznn  8338  zeo  8343  elnn1uz2  8544  qreccl  8576  qdivcl  8577  irrmul  8581  rphalfcl  8610  rpnegap  8615  ltpnf  8702  nltmnf  8709  pnfge  8710  xlt0neg1  8751  xle0neg1  8753  elioopnf  8836  elicopnf  8838  iccshftri  8863  iccshftli  8865  iccdili  8867  icccntri  8869  fzprval  8944  fzofzp1  9083  fzostep1  9093  flqge0nn0  9135  flqge1nn  9136  fldiv4p1lem1div2  9147  frecuzrdgsuc  9201  expivallem  9256  expival  9257  exp1  9261  qexpclz  9276  nn0sqcl  9282  expeq0  9286  expubnd  9311  sqval  9312  sqeq0  9317  resqcl  9321  zsqcl  9324  binom21  9363  shftfibg  9421  shftfib  9424  reim0  9461  imval2  9494  cjap0  9507  cjne0  9508  rexuz3  9588  resqrexlemover  9608  abs00  9662  abssq  9677  nn0abscl  9681  nnabscl  9696  abs2dif  9702  climshft  9825  bj-inf2vnlem1  10095