Theorem mpan2 423

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 419	1 |- ( ph -> 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:  mpanr12  437  mp3an23  1324  equs4  1718  sb4bor  1828  elvd  2735  eueq2dc  2903  sbcgf  3022  csbconstgf  3062  sbcnestg  3102  csbnestg  3103  csbnest1g  3104  ssindif0im  3474  mpteq1  4073  iinexgm  4140  mss  4211  eusv2nf  4441  eldifpw  4462  ordtriexmid  4505  onsucsssucexmid  4511  ordsucunielexmid  4515  nn0suc  4588  xpss1  4721  xpiindim  4748  reldm0  4829  elrnmpt1s  4861  resdm  4930  resid  4947  eliniseg  4981  trinxp  5004  inimasn  5028  ssrnres  5053  cnveq0  5067  coi2  5127  relrelss  5137  funcnvres  5271  funimaex  5283  fnresin1  5312  fnresin2  5313  fresin  5376  dffv3g  5492  ssimaex  5557  dmfco  5564  fvmpt  5573  fsn  5668  fsn2  5670  elabrex  5737  f1elima  5752  2ndconst  6201  tposfun  6239  tpostpos2  6244  tfrexlem  6313  tfri3  6346  rdgruledefgg  6354  rdgss  6362  frecsuclem  6385  frecrdg  6387  oa0  6436  om0  6437  oei0  6438  oav2  6442  oa1suc  6446  nnmsucr  6467  nnm1  6504  nnm2  6505  ecelqsg  6566  ecidg  6577  xpider  6584  qsel  6590  mapdm0  6641  map0e  6664  mapsnconst  6672  ixpsnf1o  6714  map1  6790  xp1en  6801  xpcomco  6804  xpmapenlem  6827  findcard2s  6868  findcard2d  6869  findcard2sd  6870  exmidpw  6886  fidcenumlemr  6932  sbthlem7  6940  eqinfti  6997  djueq1  7017  omp1eomlem  7071  endjusym  7073  eninl  7074  eninr  7075  difinfsn  7077  finomni  7116  pm54.43  7167  exmidonfinlem  7170  mulidpi  7280  nlt1pig  7303  indpi  7304  halfnqq  7372  archnqq  7379  prarloclemarch  7380  prarloclemarch2  7381  nnnq  7384  nq0a0  7419  addpinq1  7426  prarloclemlt  7455  prarloclemlo  7456  prarloclem3  7459  prarloclemcalc  7464  nqprm  7504  addnqpr1  7524  1idprl  7552  1idpru  7553  1idpr  7554  recexprlem1ssl  7595  recexprlem1ssu  7596  ltmprr  7604  0idsr  7729  1idsr  7730  00sr  7731  pn0sr  7733  negexsr  7734  recexgt0sr  7735  ltm1sr  7739  archsr  7744  prsrcl  7746  prsradd  7748  mappsrprg  7766  map2psrprg  7767  elrealeu  7791  pitonnlem1p1  7808  peano2nnnn  7815  ax1rid  7839  axcnre  7843  peano5nnnn  7854  peano2cn  8054  peano2re  8055  addid2  8058  subid  8138  subid1  8139  negid  8166  negeq0  8173  peano2cnm  8185  peano2rem  8186  mul01  8308  lt0neg1  8387  le0neg1  8389  recexre  8497  inelr  8503  rimul  8504  reapmul1  8514  apsqgt0  8520  mulge0  8538  negap0  8549  divvalap  8591  rerecclap  8647  div2negap  8652  divgt0i2i  8833  peano5nni  8881  nnge1  8901  times2  9007  addltmul  9114  nn0p1nn  9174  peano2nn0  9175  nn0lele2xi  9186  znnnlt1  9260  nn0lt10b  9292  prime  9311  msqznn  9312  zeo  9317  elnn1uz2  9566  qreccl  9601  qdivcl  9602  irrmul  9606  rphalfcl  9638  rpnegap  9643  zgt1rpn0n1  9652  ltpnf  9737  nltmnf  9745  pnfge  9746  xlt0neg1  9795  xle0neg1  9797  xaddpnf1  9803  xaddmnf1  9805  xaddid1  9819  xsubge0  9838  xleaddadd  9844  elioopnf  9924  elicopnf  9926  iccshftri  9952  iccshftli  9954  iccdili  9956  icccntri  9958  fzprval  10038  fzofzp1  10183  fzostep1  10193  flqge0nn0  10249  flqge1nn  10250  fldiv4p1lem1div2  10261  exp1  10482  qexpclz  10497  nn0sqcl  10503  expeq0  10507  expubnd  10533  sqval  10534  sqeq0  10539  resqcl  10543  zsqcl  10546  iexpcyc  10580  binom21  10588  bcnn  10691  bcn2  10698  bcn2p1  10704  bcnm1  10706  fihasheq0  10728  hashsng  10733  fihashen1  10734  fimaxq  10762  shftfibg  10784  shftfib  10787  reim0  10825  imval2  10858  cjap0  10871  cjne0  10872  rexuz3  10954  resqrexlemover  10974  abssq  11045  nn0abscl  11049  nnabscl  11064  abs2dif  11070  max0addsup  11183  climshft  11267  bcxmas  11452  efgt1p2  11658  efgt1p  11659  efi4p  11680  resin4p  11681  recos4p  11682  sinbnd  11715  cosbnd  11716  dvdsval2  11752  zdvdsdc  11774  dvdsmul2  11776  dvdsmulcr  11783  dvdsabseq  11807  divconjdvds  11809  alzdvds  11814  fzo0dvdseq  11817  odd2np1lem  11831  mod2eq1n2dvds  11838  flodddiv4  11893  flodddiv4t2lthalf  11896  gcdmndc  11899  gcd0id  11934  gcd1  11942  dfgcd2  11969  gcdmultiple  11975  gcdmultiplez  11976  dvdssq  11986  lcmmndc  12016  lcm0val  12019  dvdslcm  12023  lcmeq0  12025  lcmgcd  12032  lcmdvds  12033  lcmid  12034  lcm1  12035  cncongr2  12058  isprm3  12072  prm2orodd  12080  sqrt2irrap  12134  phiprm  12177  pc0  12258  pcdvdstr  12280  unennn  12352  ennnfonelemim  12379  ctinfom  12383  ctinf  12385  enctlem  12387  ressid  12479  elrestr  12587  0opn  12798  topopn  12800  tgval  12843  tgvalex  12844  0cld  12906  ntropn  12911  ntrtop  12922  ntr0  12928  neipsm  12948  rest0  12973  xmetres  13176  metres  13177  mopnex  13299  tgioo  13340  cnlimcim  13434  cnlimc  13435  dvfre  13468  dveflem  13481  dvef  13482  efcn  13483  sin2pim  13528  cos2pim  13529  sinmpi  13530  cosmpi  13531  sinppi  13532  cosppi  13533  efimpi  13534  sincosq1lem  13540  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  sinq34lt0t  13546  sincosq1eq  13554  abssinper  13561  logrpap0b  13591  loglt1b  13608  rpcxp0  13613  rpcxp1  13614  rpcxpsqrt  13636  logsqrt  13637  rprelogbdiv  13669  lgs0  13708  lgs2  13712  lgsneg  13719  lgsdilem  13722  lgsdir2lem2  13724  lgsdir2lem4  13726  lgsdir2lem5  13727  lgsne0  13733  bj-inf2vnlem1  14005  pwle2  14031  pwf1oexmid  14032  exmid1stab  14033  nninfsellemeqinf  14049  sbthom  14058  iswomninnlem  14081  redc0  14089