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  1342  equs4  1748  sb4bor  1858  elvd  2777  eueq2dc  2946  sbcgf  3066  csbconstgf  3106  sbcnestg  3147  csbnestg  3148  csbnest1g  3149  ssindif0im  3520  mpteq1  4128  iinexgm  4198  exmid1stab  4252  mss  4270  eusv2nf  4503  eldifpw  4524  ordtriexmid  4569  onsucsssucexmid  4575  ordsucunielexmid  4579  nn0suc  4652  xpss1  4785  xpiindim  4815  reldm0  4896  elrnmpt1s  4928  resdm  4998  resid  5016  eliniseg  5052  trinxp  5076  inimasn  5100  ssrnres  5125  cnveq0  5139  coi2  5199  relrelss  5209  funcnvres  5347  funimaex  5359  fnresin1  5390  fnresin2  5391  fresin  5454  dffv3g  5572  ssimaex  5640  dmfco  5647  fvmpt  5656  fsn  5752  fsn2  5754  funop  5763  elabrex  5826  elabrexg  5827  f1elima  5842  2ndconst  6308  tposfun  6346  tpostpos2  6351  tfrexlem  6420  tfri3  6453  rdgruledefgg  6461  rdgss  6469  frecsuclem  6492  frecrdg  6494  oa0  6543  om0  6544  oei0  6545  oav2  6549  oa1suc  6553  nnmsucr  6574  nnm1  6611  nnm2  6612  ecelqsg  6675  ecidg  6686  xpider  6693  qsel  6699  mapdm0  6750  map0e  6773  mapsnconst  6781  ixpsnf1o  6823  map1  6904  xp1en  6918  xpcomco  6921  xpmapenlem  6946  findcard2s  6987  findcard2d  6988  findcard2sd  6989  exmidpw  7005  residfi  7042  fidcenumlemr  7057  sbthlem7  7065  eqinfti  7122  djueq1  7142  omp1eomlem  7196  endjusym  7198  eninl  7199  eninr  7200  difinfsn  7202  finomni  7242  pm54.43  7298  exmidonfinlem  7301  2onetap  7367  mulidpi  7431  nlt1pig  7454  indpi  7455  halfnqq  7523  archnqq  7530  prarloclemarch  7531  prarloclemarch2  7532  nnnq  7535  nq0a0  7570  addpinq1  7577  prarloclemlt  7606  prarloclemlo  7607  prarloclem3  7610  prarloclemcalc  7615  nqprm  7655  addnqpr1  7675  1idprl  7703  1idpru  7704  1idpr  7705  recexprlem1ssl  7746  recexprlem1ssu  7747  ltmprr  7755  0idsr  7880  1idsr  7881  00sr  7882  pn0sr  7884  negexsr  7885  recexgt0sr  7886  ltm1sr  7890  archsr  7895  prsrcl  7897  prsradd  7899  mappsrprg  7917  map2psrprg  7918  elrealeu  7942  pitonnlem1p1  7959  peano2nnnn  7966  ax1rid  7990  axcnre  7994  peano5nnnn  8005  peano2cn  8207  peano2re  8208  addlid  8211  subid  8291  subid1  8292  negid  8319  negeq0  8326  peano2cnm  8338  peano2rem  8339  mul01  8461  lt0neg1  8541  le0neg1  8543  recexre  8651  inelr  8657  rimul  8658  reapmul1  8668  apsqgt0  8674  mulge0  8692  negap0  8703  divvalap  8747  rerecclap  8803  div2negap  8808  divgt0i2i  8990  peano5nni  9039  nnge1  9059  times2  9165  addltmul  9274  nn0p1nn  9334  peano2nn0  9335  nn0lele2xi  9346  znnnlt1  9420  nn0lt10b  9453  prime  9472  msqznn  9473  zeo  9478  elnn1uz2  9728  qreccl  9763  qdivcl  9764  irrmul  9768  rphalfcl  9803  rpnegap  9808  zgt1rpn0n1  9817  ltpnf  9902  nltmnf  9910  pnfge  9911  xlt0neg1  9960  xle0neg1  9962  xaddpnf1  9968  xaddmnf1  9970  xaddid1  9984  xsubge0  10003  xleaddadd  10009  elioopnf  10089  elicopnf  10091  iccshftri  10117  iccshftli  10119  iccdili  10121  icccntri  10123  fzprval  10204  fzofzp1  10356  fzostep1  10366  flqge0nn0  10436  flqge1nn  10437  fldiv4p1lem1div2  10448  exp1  10690  qexpclz  10705  nn0sqcl  10711  expeq0  10715  expubnd  10741  sqval  10742  sqeq0  10747  resqcl  10752  zsqcl  10755  iexpcyc  10789  binom21  10797  bcnn  10902  bcn2  10909  bcn2p1  10915  bcnm1  10917  fihasheq0  10938  hashsng  10943  fihashen1  10944  fimaxq  10972  iswrddm0  11018  ccatval2  11054  ccatsymb  11058  ccatrid  11063  eqs1  11082  s111  11085  swrdnd  11112  shftfibg  11131  shftfib  11134  reim0  11172  imval2  11205  cjap0  11218  cjne0  11219  rexuz3  11301  resqrexlemover  11321  abssq  11392  nn0abscl  11396  nnabscl  11411  abs2dif  11417  max0addsup  11530  climshft  11615  bcxmas  11800  efgt1p2  12006  efgt1p  12007  efi4p  12028  resin4p  12029  recos4p  12030  sinbnd  12063  cosbnd  12064  dvdsval2  12101  zdvdsdc  12123  dvdsmul2  12125  dvdsmulcr  12132  dvdsabseq  12158  divconjdvds  12160  alzdvds  12165  fzo0dvdseq  12168  odd2np1lem  12183  mod2eq1n2dvds  12190  flodddiv4  12247  flodddiv4t2lthalf  12250  bits0  12259  bitsp1o  12264  gcdmndc  12276  gcd0id  12300  gcd1  12308  dfgcd2  12335  gcdmultiple  12341  gcdmultiplez  12342  dvdssq  12352  lcmmndc  12384  lcm0val  12387  dvdslcm  12391  lcmeq0  12393  lcmgcd  12400  lcmdvds  12401  lcmid  12402  lcm1  12403  cncongr2  12426  isprm3  12440  prm2orodd  12448  sqrt2irrap  12502  phiprm  12545  pc0  12627  pcxqcl  12635  pcdvdstr  12650  unennn  12768  ennnfonelemim  12795  ctinfom  12799  ctinf  12801  enctlem  12803  elrestr  13079  tgval  13094  tgvalex  13095  xpsfrnel  13176  xpsfeq  13177  xpscf  13179  mulg1  13465  mulgnegnn  13468  ghmghmrn  13599  subrngintm  13974  subrgintm  14005  lsp0  14185  mulgrhm2  14372  zlmlemg  14390  zlmsca  14394  0opn  14478  topopn  14480  0cld  14584  ntropn  14589  ntrtop  14600  ntr0  14606  neipsm  14626  rest0  14651  xmetres  14854  metres  14855  mopnex  14977  tgioo  15026  cnlimcim  15143  cnlimc  15144  dvfre  15182  dveflem  15198  dvef  15199  efcn  15240  sin2pim  15285  cos2pim  15286  sinmpi  15287  cosmpi  15288  sinppi  15289  cosppi  15290  efimpi  15291  sincosq1lem  15297  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  sinq12gt0  15302  sinq34lt0t  15303  sincosq1eq  15311  abssinper  15318  logrpap0b  15348  loglt1b  15365  rpcxp0  15370  rpcxp1  15371  rpcxpsqrt  15394  logsqrt  15395  rprelogbdiv  15429  lgs0  15490  lgs2  15494  lgsneg  15501  lgsdilem  15504  lgsdir2lem2  15506  lgsdir2lem4  15508  lgsdir2lem5  15509  lgsne0  15515  2lgslem1a2  15564  2lgslem1c  15567  bj-inf2vnlem1  15906  pwle2  15935  pwf1oexmid  15936  domomsubct  15938  nninfsellemeqinf  15953  sbthom  15965  iswomninnlem  15988  redc0  15996