Theorem mpan2 425

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mpanr12  439  mp3an23  1363  equs4  1771  sb4bor  1881  elvd  2804  eueq2dc  2976  sbcgf  3096  csbconstgf  3137  sbcnestg  3178  csbnestg  3179  csbnest1g  3180  ssindif0im  3551  mpteq1  4168  iinexgm  4238  exmid1stab  4292  mss  4312  eusv2nf  4547  eldifpw  4568  ordtriexmid  4613  onsucsssucexmid  4619  ordsucunielexmid  4623  nn0suc  4696  xpss1  4829  xpiindim  4859  reldm0  4941  elrnmpt1s  4974  resdm  5044  resid  5062  eliniseg  5098  trinxp  5122  inimasn  5146  ssrnres  5171  cnveq0  5185  coi2  5245  relrelss  5255  funcnvres  5394  funimaex  5406  fnresin1  5438  fnresin2  5439  fresin  5506  dffv3g  5625  ssimaex  5697  dmfco  5704  fvmpt  5713  fsn  5809  fsn2  5811  funop  5820  elabrex  5887  elabrexg  5888  f1elima  5903  2ndconst  6374  tposfun  6412  tpostpos2  6417  tfrexlem  6486  tfri3  6519  rdgruledefgg  6527  rdgss  6535  frecsuclem  6558  frecrdg  6560  oa0  6611  om0  6612  oei0  6613  oav2  6617  oa1suc  6621  nnmsucr  6642  nnm1  6679  nnm2  6680  ecelqsg  6743  ecidg  6754  xpider  6761  qsel  6767  mapdm0  6818  map0e  6841  mapsnconst  6849  ixpsnf1o  6891  map1  6973  dom1o  6985  xp1en  6990  xpcomco  6993  xpmapenlem  7018  findcard2s  7060  findcard2d  7061  findcard2sd  7062  exmidpw  7081  residfi  7118  fidcenumlemr  7133  sbthlem7  7141  eqinfti  7198  djueq1  7218  omp1eomlem  7272  endjusym  7274  eninl  7275  eninr  7276  difinfsn  7278  finomni  7318  pm54.43  7374  exmidonfinlem  7382  2onetap  7452  mulidpi  7516  nlt1pig  7539  indpi  7540  halfnqq  7608  archnqq  7615  prarloclemarch  7616  prarloclemarch2  7617  nnnq  7620  nq0a0  7655  addpinq1  7662  prarloclemlt  7691  prarloclemlo  7692  prarloclem3  7695  prarloclemcalc  7700  nqprm  7740  addnqpr1  7760  1idprl  7788  1idpru  7789  1idpr  7790  recexprlem1ssl  7831  recexprlem1ssu  7832  ltmprr  7840  0idsr  7965  1idsr  7966  00sr  7967  pn0sr  7969  negexsr  7970  recexgt0sr  7971  ltm1sr  7975  archsr  7980  prsrcl  7982  prsradd  7984  mappsrprg  8002  map2psrprg  8003  elrealeu  8027  pitonnlem1p1  8044  peano2nnnn  8051  ax1rid  8075  axcnre  8079  peano5nnnn  8090  peano2cn  8292  peano2re  8293  addlid  8296  subid  8376  subid1  8377  negid  8404  negeq0  8411  peano2cnm  8423  peano2rem  8424  mul01  8546  lt0neg1  8626  le0neg1  8628  recexre  8736  inelr  8742  rimul  8743  reapmul1  8753  apsqgt0  8759  mulge0  8777  negap0  8788  divvalap  8832  rerecclap  8888  div2negap  8893  divgt0i2i  9075  peano5nni  9124  nnge1  9144  times2  9250  addltmul  9359  nn0p1nn  9419  peano2nn0  9420  nn0lele2xi  9431  znnnlt1  9505  nn0lt10b  9538  prime  9557  msqznn  9558  zeo  9563  elnn1uz2  9814  qreccl  9849  qdivcl  9850  irrmul  9854  rphalfcl  9889  rpnegap  9894  zgt1rpn0n1  9903  ltpnf  9988  nltmnf  9996  pnfge  9997  xlt0neg1  10046  xle0neg1  10048  xaddpnf1  10054  xaddmnf1  10056  xaddid1  10070  xsubge0  10089  xleaddadd  10095  elioopnf  10175  elicopnf  10177  iccshftri  10203  iccshftli  10205  iccdili  10207  icccntri  10209  fzprval  10290  fzofzp1  10445  fzostep1  10455  flqge0nn0  10525  flqge1nn  10526  fldiv4p1lem1div2  10537  exp1  10779  qexpclz  10794  nn0sqcl  10800  expeq0  10804  expubnd  10830  sqval  10831  sqeq0  10836  resqcl  10841  zsqcl  10844  iexpcyc  10878  binom21  10886  bcnn  10991  bcn2  10998  bcn2p1  11004  bcnm1  11006  fihasheq0  11027  hashsng  11032  fihashen1  11033  fimaxq  11062  iswrddm0  11108  ccatval2  11146  ccatsymb  11150  ccatrid  11155  eqs1  11176  s111  11179  swrdnd  11207  pfx00g  11223  shftfibg  11347  shftfib  11350  reim0  11388  imval2  11421  cjap0  11434  cjne0  11435  rexuz3  11517  resqrexlemover  11537  abssq  11608  nn0abscl  11612  nnabscl  11627  abs2dif  11633  max0addsup  11746  climshft  11831  bcxmas  12016  efgt1p2  12222  efgt1p  12223  efi4p  12244  resin4p  12245  recos4p  12246  sinbnd  12279  cosbnd  12280  dvdsval2  12317  zdvdsdc  12339  dvdsmul2  12341  dvdsmulcr  12348  dvdsabseq  12374  divconjdvds  12376  alzdvds  12381  fzo0dvdseq  12384  odd2np1lem  12399  mod2eq1n2dvds  12406  flodddiv4  12463  flodddiv4t2lthalf  12466  bits0  12475  bitsp1o  12480  gcdmndc  12492  gcd0id  12516  gcd1  12524  dfgcd2  12551  gcdmultiple  12557  gcdmultiplez  12558  dvdssq  12568  lcmmndc  12600  lcm0val  12603  dvdslcm  12607  lcmeq0  12609  lcmgcd  12616  lcmdvds  12617  lcmid  12618  lcm1  12619  cncongr2  12642  isprm3  12656  prm2orodd  12664  sqrt2irrap  12718  phiprm  12761  pc0  12843  pcxqcl  12851  pcdvdstr  12866  unennn  12984  ennnfonelemim  13011  ctinfom  13015  ctinf  13017  enctlem  13019  elrestr  13296  tgval  13311  tgvalex  13312  xpsfrnel  13393  xpsfeq  13394  xpscf  13396  mulg1  13682  mulgnegnn  13685  ghmghmrn  13816  subrngintm  14192  subrgintm  14223  lsp0  14403  mulgrhm2  14590  zlmlemg  14608  zlmsca  14612  0opn  14696  topopn  14698  0cld  14802  ntropn  14807  ntrtop  14818  ntr0  14824  neipsm  14844  rest0  14869  xmetres  15072  metres  15073  mopnex  15195  tgioo  15244  cnlimcim  15361  cnlimc  15362  dvfre  15400  dveflem  15416  dvef  15417  efcn  15458  sin2pim  15503  cos2pim  15504  sinmpi  15505  cosmpi  15506  sinppi  15507  cosppi  15508  efimpi  15509  sincosq1lem  15515  sincosq2sgn  15517  sincosq3sgn  15518  sincosq4sgn  15519  sinq12gt0  15520  sinq34lt0t  15521  sincosq1eq  15529  abssinper  15536  logrpap0b  15566  loglt1b  15583  rpcxp0  15588  rpcxp1  15589  rpcxpsqrt  15612  logsqrt  15613  rprelogbdiv  15647  lgs0  15708  lgs2  15712  lgsneg  15719  lgsdilem  15722  lgsdir2lem2  15724  lgsdir2lem4  15726  lgsdir2lem5  15727  lgsne0  15733  2lgslem1a2  15782  2lgslem1c  15785  upgr0eop  15938  uspgrushgr  15994  usgruspgr  15997  wlklenvclwlk  16119  upgr2wlkdc  16121  bj-inf2vnlem1  16416  pwle2  16451  pwf1oexmid  16452  domomsubct  16454  nninfsellemeqinf  16470  sbthom  16482  iswomninnlem  16505  redc0  16513