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  5504  dffv3g  5623  ssimaex  5695  dmfco  5702  fvmpt  5711  fsn  5807  fsn2  5809  funop  5818  elabrex  5881  elabrexg  5882  f1elima  5897  2ndconst  6368  tposfun  6406  tpostpos2  6411  tfrexlem  6480  tfri3  6513  rdgruledefgg  6521  rdgss  6529  frecsuclem  6552  frecrdg  6554  oa0  6603  om0  6604  oei0  6605  oav2  6609  oa1suc  6613  nnmsucr  6634  nnm1  6671  nnm2  6672  ecelqsg  6735  ecidg  6746  xpider  6753  qsel  6759  mapdm0  6810  map0e  6833  mapsnconst  6841  ixpsnf1o  6883  map1  6965  dom1o  6977  xp1en  6982  xpcomco  6985  xpmapenlem  7010  findcard2s  7052  findcard2d  7053  findcard2sd  7054  exmidpw  7070  residfi  7107  fidcenumlemr  7122  sbthlem7  7130  eqinfti  7187  djueq1  7207  omp1eomlem  7261  endjusym  7263  eninl  7264  eninr  7265  difinfsn  7267  finomni  7307  pm54.43  7363  exmidonfinlem  7371  2onetap  7441  mulidpi  7505  nlt1pig  7528  indpi  7529  halfnqq  7597  archnqq  7604  prarloclemarch  7605  prarloclemarch2  7606  nnnq  7609  nq0a0  7644  addpinq1  7651  prarloclemlt  7680  prarloclemlo  7681  prarloclem3  7684  prarloclemcalc  7689  nqprm  7729  addnqpr1  7749  1idprl  7777  1idpru  7778  1idpr  7779  recexprlem1ssl  7820  recexprlem1ssu  7821  ltmprr  7829  0idsr  7954  1idsr  7955  00sr  7956  pn0sr  7958  negexsr  7959  recexgt0sr  7960  ltm1sr  7964  archsr  7969  prsrcl  7971  prsradd  7973  mappsrprg  7991  map2psrprg  7992  elrealeu  8016  pitonnlem1p1  8033  peano2nnnn  8040  ax1rid  8064  axcnre  8068  peano5nnnn  8079  peano2cn  8281  peano2re  8282  addlid  8285  subid  8365  subid1  8366  negid  8393  negeq0  8400  peano2cnm  8412  peano2rem  8413  mul01  8535  lt0neg1  8615  le0neg1  8617  recexre  8725  inelr  8731  rimul  8732  reapmul1  8742  apsqgt0  8748  mulge0  8766  negap0  8777  divvalap  8821  rerecclap  8877  div2negap  8882  divgt0i2i  9064  peano5nni  9113  nnge1  9133  times2  9239  addltmul  9348  nn0p1nn  9408  peano2nn0  9409  nn0lele2xi  9420  znnnlt1  9494  nn0lt10b  9527  prime  9546  msqznn  9547  zeo  9552  elnn1uz2  9802  qreccl  9837  qdivcl  9838  irrmul  9842  rphalfcl  9877  rpnegap  9882  zgt1rpn0n1  9891  ltpnf  9976  nltmnf  9984  pnfge  9985  xlt0neg1  10034  xle0neg1  10036  xaddpnf1  10042  xaddmnf1  10044  xaddid1  10058  xsubge0  10077  xleaddadd  10083  elioopnf  10163  elicopnf  10165  iccshftri  10191  iccshftli  10193  iccdili  10195  icccntri  10197  fzprval  10278  fzofzp1  10433  fzostep1  10443  flqge0nn0  10513  flqge1nn  10514  fldiv4p1lem1div2  10525  exp1  10767  qexpclz  10782  nn0sqcl  10788  expeq0  10792  expubnd  10818  sqval  10819  sqeq0  10824  resqcl  10829  zsqcl  10832  iexpcyc  10866  binom21  10874  bcnn  10979  bcn2  10986  bcn2p1  10992  bcnm1  10994  fihasheq0  11015  hashsng  11020  fihashen1  11021  fimaxq  11049  iswrddm0  11095  ccatval2  11133  ccatsymb  11137  ccatrid  11142  eqs1  11161  s111  11164  swrdnd  11191  pfx00g  11207  shftfibg  11331  shftfib  11334  reim0  11372  imval2  11405  cjap0  11418  cjne0  11419  rexuz3  11501  resqrexlemover  11521  abssq  11592  nn0abscl  11596  nnabscl  11611  abs2dif  11617  max0addsup  11730  climshft  11815  bcxmas  12000  efgt1p2  12206  efgt1p  12207  efi4p  12228  resin4p  12229  recos4p  12230  sinbnd  12263  cosbnd  12264  dvdsval2  12301  zdvdsdc  12323  dvdsmul2  12325  dvdsmulcr  12332  dvdsabseq  12358  divconjdvds  12360  alzdvds  12365  fzo0dvdseq  12368  odd2np1lem  12383  mod2eq1n2dvds  12390  flodddiv4  12447  flodddiv4t2lthalf  12450  bits0  12459  bitsp1o  12464  gcdmndc  12476  gcd0id  12500  gcd1  12508  dfgcd2  12535  gcdmultiple  12541  gcdmultiplez  12542  dvdssq  12552  lcmmndc  12584  lcm0val  12587  dvdslcm  12591  lcmeq0  12593  lcmgcd  12600  lcmdvds  12601  lcmid  12602  lcm1  12603  cncongr2  12626  isprm3  12640  prm2orodd  12648  sqrt2irrap  12702  phiprm  12745  pc0  12827  pcxqcl  12835  pcdvdstr  12850  unennn  12968  ennnfonelemim  12995  ctinfom  12999  ctinf  13001  enctlem  13003  elrestr  13280  tgval  13295  tgvalex  13296  xpsfrnel  13377  xpsfeq  13378  xpscf  13380  mulg1  13666  mulgnegnn  13669  ghmghmrn  13800  subrngintm  14176  subrgintm  14207  lsp0  14387  mulgrhm2  14574  zlmlemg  14592  zlmsca  14596  0opn  14680  topopn  14682  0cld  14786  ntropn  14791  ntrtop  14802  ntr0  14808  neipsm  14828  rest0  14853  xmetres  15056  metres  15057  mopnex  15179  tgioo  15228  cnlimcim  15345  cnlimc  15346  dvfre  15384  dveflem  15400  dvef  15401  efcn  15442  sin2pim  15487  cos2pim  15488  sinmpi  15489  cosmpi  15490  sinppi  15491  cosppi  15492  efimpi  15493  sincosq1lem  15499  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  sinq12gt0  15504  sinq34lt0t  15505  sincosq1eq  15513  abssinper  15520  logrpap0b  15550  loglt1b  15567  rpcxp0  15572  rpcxp1  15573  rpcxpsqrt  15596  logsqrt  15597  rprelogbdiv  15631  lgs0  15692  lgs2  15696  lgsneg  15703  lgsdilem  15706  lgsdir2lem2  15708  lgsdir2lem4  15710  lgsdir2lem5  15711  lgsne0  15717  2lgslem1a2  15766  2lgslem1c  15769  upgr0eop  15922  uspgrushgr  15978  usgruspgr  15981  wlklenvclwlk  16084  bj-inf2vnlem1  16333  pwle2  16364  pwf1oexmid  16365  domomsubct  16367  nninfsellemeqinf  16382  sbthom  16394  iswomninnlem  16417  redc0  16425