Theorem mpan2 415

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 412	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  mpanr12  429  mp3an23  1260  equs4  1653  sb4bor  1756  eueq2dc  2765  sbcgf  2881  csbconstgf  2919  sbcnestg  2955  csbnestg  2956  csbnest1g  2957  ssindif0im  3303  mpteq1  3862  iinexgm  3929  mss  3981  eusv2nf  4206  eldifpw  4226  ordtriexmid  4265  onsucsssucexmid  4270  ordsucunielexmid  4274  nn0suc  4345  xpss1  4466  xpiindim  4491  reldm0  4571  elrnmpt1s  4602  resdm  4667  resid  4682  eliniseg  4715  trinxp  4738  inimasn  4761  ssrnres  4783  cnveq0  4797  coi2  4857  relrelss  4864  funcnvres  4992  funimaex  5004  fnresin1  5033  fnresin2  5034  fresin  5088  dffv3g  5194  ssimaex  5255  dmfco  5262  fvmpt  5270  fsn  5356  fsn2  5358  elabrex  5418  f1elima  5433  2ndconst  5863  tposfun  5898  tpostpos2  5903  tfrexlem  5971  tfri3  5976  rdgruledefgg  5985  rdgss  5993  frecsuclem3  6013  frecrdg  6015  oa0  6060  om0  6061  oei0  6062  oav2  6066  oa1suc  6070  nnmsucr  6090  nnm1  6120  nnm2  6121  ecelqsg  6182  ecidg  6193  xpiderm  6200  qsel  6206  xp1en  6320  xpcomco  6323  findcard2s  6374  findcard2d  6375  findcard2sd  6376  eqinfti  6433  pm54.43  6459  mulidpi  6508  nlt1pig  6531  indpi  6532  halfnqq  6600  archnqq  6607  prarloclemarch  6608  prarloclemarch2  6609  nnnq  6612  nq0a0  6647  addpinq1  6654  prarloclemlt  6683  prarloclemlo  6684  prarloclem3  6687  prarloclemcalc  6692  nqprm  6732  addnqpr1  6752  1idprl  6780  1idpru  6781  1idpr  6782  recexprlem1ssl  6823  recexprlem1ssu  6824  ltmprr  6832  0idsr  6944  1idsr  6945  00sr  6946  pn0sr  6948  negexsr  6949  recexgt0sr  6950  archsr  6958  prsrcl  6960  prsradd  6962  elrealeu  6998  pitonnlem1p1  7014  peano2nnnn  7021  ax1rid  7043  axcnre  7047  peano5nnnn  7058  peano2cn  7243  peano2re  7244  addid2  7247  subid  7327  subid1  7328  negid  7355  negeq0  7362  peano2cnm  7374  peano2rem  7375  mul01  7493  lt0neg1  7572  le0neg1  7574  recexre  7678  inelr  7684  rimul  7685  reapmul1  7695  apsqgt0  7701  mulge0  7719  negap0  7729  divvalap  7762  rerecclap  7818  div2negap  7823  divgt0i2i  7995  peano5nni  8042  nnge1  8062  times2  8161  addltmul  8267  nn0p1nn  8327  peano2nn0  8328  nn0lele2xi  8339  znnnlt1  8399  nn0lt10b  8428  prime  8446  msqznn  8447  zeo  8452  elnn1uz2  8694  qreccl  8727  qdivcl  8728  irrmul  8732  rphalfcl  8761  rpnegap  8766  ltpnf  8856  nltmnf  8863  pnfge  8864  xlt0neg1  8905  xle0neg1  8907  elioopnf  8990  elicopnf  8992  iccshftri  9017  iccshftli  9019  iccdili  9021  icccntri  9023  fzprval  9099  fzofzp1  9236  fzostep1  9246  flqge0nn0  9295  flqge1nn  9296  fldiv4p1lem1div2  9307  frecuzrdgsuc  9417  expivallem  9477  expival  9478  exp1  9482  qexpclz  9497  nn0sqcl  9503  expeq0  9507  expubnd  9533  sqval  9534  sqeq0  9539  resqcl  9543  zsqcl  9546  iexpcyc  9579  binom21  9586  bcnn  9684  bcn2  9691  bcn2p1  9697  bcnm1  9699  shftfibg  9708  shftfib  9711  reim0  9748  imval2  9781  cjap0  9794  cjne0  9795  rexuz3  9876  resqrexlemover  9896  abs00  9950  abssq  9967  nn0abscl  9971  nnabscl  9986  abs2dif  9992  max0addsup  10105  climshft  10143  dvdsval2  10198  zdvdsdc  10216  dvdsmul2  10218  dvdsmulcr  10225  dvdsabseq  10247  divconjdvds  10249  alzdvds  10254  fzo0dvdseq  10257  odd2np1lem  10271  mod2eq1n2dvds  10279  flodddiv4  10334  flodddiv4t2lthalf  10337  gcdmndc  10340  gcd0id  10370  gcd1  10378  dfgcd2  10403  gcdmultiple  10409  gcdmultiplez  10410  dvdssq  10420  lcmmndc  10444  lcm0val  10447  dvdslcm  10451  lcmeq0  10453  lcmgcd  10460  lcmdvds  10461  lcmid  10462  lcm1  10463  cncongr2  10486  isprm3  10500  prm2orodd  10508  sqrt2irrap  10558  bj-inf2vnlem1  10765