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  1366  equs4  1773  sb4bor  1884  elvd  2818  eueq2dc  2990  sbcgf  3110  csbconstgf  3151  sbcnestg  3192  csbnestg  3193  csbnest1g  3194  ssindif0im  3568  mpteq1  4194  iinexgm  4266  exmid1stab  4321  mss  4342  eusv2nf  4577  eldifpw  4598  ordtriexmid  4643  onsucsssucexmid  4649  ordsucunielexmid  4653  nn0suc  4726  xpss1  4860  xpiindim  4892  reldm0  4974  elrnmpt1s  5007  resdm  5077  resid  5095  eliniseg  5132  trinxp  5156  inimasn  5180  ssrnres  5205  cnveq0  5219  coi2  5279  relrelss  5289  funcnvres  5429  funimaex  5441  fnresin1  5473  fnresin2  5474  fresin  5543  dffv3g  5666  ssimaex  5738  dmfco  5745  fvmpt  5754  fsn  5849  fsn2  5851  funop  5861  elabrex  5930  elabrexg  5931  f1elima  5946  2ndconst  6418  tposfun  6491  tpostpos2  6496  tfrexlem  6565  tfri3  6598  rdgruledefgg  6606  rdgss  6614  frecsuclem  6637  frecrdg  6639  oa0  6690  om0  6691  oei0  6692  oav2  6696  oa1suc  6700  nnmsucr  6721  nnm1  6758  nnm2  6759  ecelqsg  6822  ecidg  6833  xpider  6840  qsel  6846  mapdm0  6897  map0e  6920  mapsnconst  6929  ixpsnf1o  6971  map1  7054  dom1o  7069  xp1en  7074  xpcomco  7077  xpmapenlem  7102  findcard2s  7147  findcard2d  7148  findcard2sd  7149  exmidpw  7168  residfi  7207  fidcenumlemr  7225  sbthlem7  7233  eqinfti  7311  djueq1  7331  omp1eomlem  7385  endjusym  7387  eninl  7388  eninr  7389  difinfsn  7391  finomni  7431  pm54.43  7487  exmidonfinlem  7496  2onetap  7569  mulidpi  7633  nlt1pig  7656  indpi  7657  halfnqq  7725  archnqq  7732  prarloclemarch  7733  prarloclemarch2  7734  nnnq  7737  nq0a0  7772  addpinq1  7779  prarloclemlt  7808  prarloclemlo  7809  prarloclem3  7812  prarloclemcalc  7817  nqprm  7857  addnqpr1  7877  1idprl  7905  1idpru  7906  1idpr  7907  recexprlem1ssl  7948  recexprlem1ssu  7949  ltmprr  7957  0idsr  8082  1idsr  8083  00sr  8084  pn0sr  8086  negexsr  8087  recexgt0sr  8088  ltm1sr  8092  archsr  8097  prsrcl  8099  prsradd  8101  mappsrprg  8119  map2psrprg  8120  elrealeu  8144  pitonnlem1p1  8161  peano2nnnn  8168  ax1rid  8192  axcnre  8196  peano5nnnn  8207  peano2cn  8408  peano2re  8409  addlid  8412  subid  8492  subid1  8493  negid  8520  negeq0  8527  peano2cnm  8539  peano2rem  8540  mul01  8662  lt0neg1  8742  le0neg1  8744  recexre  8852  inelr  8858  rimul  8859  reapmul1  8869  apsqgt0  8875  mulge0  8893  negap0  8904  divvalap  8948  rerecclap  9004  div2negap  9009  divgt0i2i  9191  peano5nni  9240  nnge1  9260  times2  9366  addltmul  9475  nn0p1nn  9535  peano2nn0  9536  nn0lele2xi  9547  fcdmnn0supp  9548  fcdmnn0fsupp  9549  fcdmnn0suppg  9550  znnnlt1  9625  nn0lt10b  9658  prime  9677  msqznn  9678  zeo  9683  elnn1uz2  9939  qreccl  9974  qdivcl  9975  irrmul  9979  rphalfcl  10014  rpnegap  10019  zgt1rpn0n1  10028  ltpnf  10113  nltmnf  10121  pnfge  10122  xlt0neg1  10171  xle0neg1  10173  xaddpnf1  10179  xaddmnf1  10181  xaddid1  10195  xsubge0  10214  xleaddadd  10220  elioopnf  10300  elicopnf  10302  iccshftri  10328  iccshftli  10330  iccdili  10332  icccntri  10334  fzprval  10416  fzofzp1  10572  fzostep1  10583  flqge0nn0  10653  flqge1nn  10654  fldiv4p1lem1div2  10665  exp1  10907  qexpclz  10922  nn0sqcl  10928  expeq0  10932  expubnd  10958  sqval  10959  sqeq0  10964  resqcl  10969  zsqcl  10972  iexpcyc  11006  binom21  11014  bcnn  11119  bcn2  11126  bcn2p1  11133  bcnm1  11135  fihasheq0  11156  hashsng  11161  fihashen1  11162  fimaxq  11194  iswrddm0  11248  ccatval2  11286  ccatsymb  11290  ccatrid  11295  eqs1  11316  s111  11319  swrdnd  11351  pfx00g  11367  shftfibg  11505  shftfib  11508  reim0  11546  imval2  11579  cjap0  11592  cjne0  11593  rexuz3  11675  resqrexlemover  11695  abssq  11766  nn0abscl  11770  nnabscl  11785  abs2dif  11791  max0addsup  11904  climshft  11989  bcxmas  12175  efgt1p2  12381  efgt1p  12382  efi4p  12403  resin4p  12404  recos4p  12405  sinbnd  12438  cosbnd  12439  dvdsval2  12476  zdvdsdc  12498  dvdsmul2  12500  dvdsmulcr  12507  dvdsabseq  12533  divconjdvds  12535  alzdvds  12540  fzo0dvdseq  12543  odd2np1lem  12558  mod2eq1n2dvds  12565  flodddiv4  12622  flodddiv4t2lthalf  12625  bits0  12634  bitsp1o  12639  gcdmndc  12651  gcd0id  12675  gcd1  12683  dfgcd2  12710  gcdmultiple  12716  gcdmultiplez  12717  dvdssq  12727  lcmmndc  12759  lcm0val  12762  dvdslcm  12766  lcmeq0  12768  lcmgcd  12775  lcmdvds  12776  lcmid  12777  lcm1  12778  cncongr2  12801  isprm3  12815  prm2orodd  12823  sqrt2irrap  12877  phiprm  12920  pc0  13002  pcxqcl  13010  pcdvdstr  13025  ballotfilem2  13142  unennn  13148  ennnfonelemim  13175  ctinfom  13179  ctinf  13181  enctlem  13183  elrestr  13460  tgval  13475  tgvalex  13476  xpsfrnel  13557  xpsfeq  13558  xpscf  13560  mulg1  13846  mulgnegnn  13849  ghmghmrn  13980  subrngintm  14357  subrgintm  14388  lsp0  14571  mulgrhm2  14758  zlmlemg  14776  zlmsca  14780  0opn  14871  topopn  14873  0cld  14977  ntropn  14982  ntrtop  14993  ntr0  14999  neipsm  15019  rest0  15044  xmetres  15247  metres  15248  mopnex  15370  tgioo  15419  cnlimcim  15536  cnlimc  15537  dvfre  15575  dveflem  15591  dvef  15592  efcn  15633  sin2pim  15678  cos2pim  15679  sinmpi  15680  cosmpi  15681  sinppi  15682  cosppi  15683  efimpi  15684  sincosq1lem  15690  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  sinq34lt0t  15696  sincosq1eq  15704  abssinper  15711  logrpap0b  15741  loglt1b  15758  rpcxp0  15763  rpcxp1  15764  rpcxpsqrt  15787  logsqrt  15788  rprelogbdiv  15822  lgs0  15886  lgs2  15890  lgsneg  15897  lgsdilem  15900  lgsdir2lem2  15902  lgsdir2lem4  15904  lgsdir2lem5  15905  lgsne0  15911  2lgslem1a2  15960  2lgslem1c  15963  upgr0eop  16117  uspgrushgr  16175  usgruspgr  16178  usgr0eop  16237  0grsubgr  16259  wlklenvclwlk  16368  upgr2wlkdc  16372  clwwlk0on0  16426  konigsbergssiedgwen  16481  bj-inf2vnlem1  16740  pwle2  16772  pwf1oexmid  16773  domomsubct  16775  nninfsellemeqinf  16794  sbthom  16806  qdiff  16833  iswomninnlem  16834  redc0  16842