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  1329  equs4  1725  sb4bor  1835  elvd  2744  eueq2dc  2912  sbcgf  3032  csbconstgf  3072  sbcnestg  3112  csbnestg  3113  csbnest1g  3114  ssindif0im  3484  mpteq1  4089  iinexgm  4156  exmid1stab  4210  mss  4228  eusv2nf  4458  eldifpw  4479  ordtriexmid  4522  onsucsssucexmid  4528  ordsucunielexmid  4532  nn0suc  4605  xpss1  4738  xpiindim  4766  reldm0  4847  elrnmpt1s  4879  resdm  4948  resid  4966  eliniseg  5000  trinxp  5024  inimasn  5048  ssrnres  5073  cnveq0  5087  coi2  5147  relrelss  5157  funcnvres  5291  funimaex  5303  fnresin1  5332  fnresin2  5333  fresin  5396  dffv3g  5513  ssimaex  5579  dmfco  5586  fvmpt  5595  fsn  5690  fsn2  5692  elabrex  5760  elabrexg  5761  f1elima  5776  2ndconst  6225  tposfun  6263  tpostpos2  6268  tfrexlem  6337  tfri3  6370  rdgruledefgg  6378  rdgss  6386  frecsuclem  6409  frecrdg  6411  oa0  6460  om0  6461  oei0  6462  oav2  6466  oa1suc  6470  nnmsucr  6491  nnm1  6528  nnm2  6529  ecelqsg  6590  ecidg  6601  xpider  6608  qsel  6614  mapdm0  6665  map0e  6688  mapsnconst  6696  ixpsnf1o  6738  map1  6814  xp1en  6825  xpcomco  6828  xpmapenlem  6851  findcard2s  6892  findcard2d  6893  findcard2sd  6894  exmidpw  6910  fidcenumlemr  6956  sbthlem7  6964  eqinfti  7021  djueq1  7041  omp1eomlem  7095  endjusym  7097  eninl  7098  eninr  7099  difinfsn  7101  finomni  7140  pm54.43  7191  exmidonfinlem  7194  2onetap  7256  mulidpi  7319  nlt1pig  7342  indpi  7343  halfnqq  7411  archnqq  7418  prarloclemarch  7419  prarloclemarch2  7420  nnnq  7423  nq0a0  7458  addpinq1  7465  prarloclemlt  7494  prarloclemlo  7495  prarloclem3  7498  prarloclemcalc  7503  nqprm  7543  addnqpr1  7563  1idprl  7591  1idpru  7592  1idpr  7593  recexprlem1ssl  7634  recexprlem1ssu  7635  ltmprr  7643  0idsr  7768  1idsr  7769  00sr  7770  pn0sr  7772  negexsr  7773  recexgt0sr  7774  ltm1sr  7778  archsr  7783  prsrcl  7785  prsradd  7787  mappsrprg  7805  map2psrprg  7806  elrealeu  7830  pitonnlem1p1  7847  peano2nnnn  7854  ax1rid  7878  axcnre  7882  peano5nnnn  7893  peano2cn  8094  peano2re  8095  addlid  8098  subid  8178  subid1  8179  negid  8206  negeq0  8213  peano2cnm  8225  peano2rem  8226  mul01  8348  lt0neg1  8427  le0neg1  8429  recexre  8537  inelr  8543  rimul  8544  reapmul1  8554  apsqgt0  8560  mulge0  8578  negap0  8589  divvalap  8633  rerecclap  8689  div2negap  8694  divgt0i2i  8876  peano5nni  8924  nnge1  8944  times2  9050  addltmul  9157  nn0p1nn  9217  peano2nn0  9218  nn0lele2xi  9229  znnnlt1  9303  nn0lt10b  9335  prime  9354  msqznn  9355  zeo  9360  elnn1uz2  9609  qreccl  9644  qdivcl  9645  irrmul  9649  rphalfcl  9683  rpnegap  9688  zgt1rpn0n1  9697  ltpnf  9782  nltmnf  9790  pnfge  9791  xlt0neg1  9840  xle0neg1  9842  xaddpnf1  9848  xaddmnf1  9850  xaddid1  9864  xsubge0  9883  xleaddadd  9889  elioopnf  9969  elicopnf  9971  iccshftri  9997  iccshftli  9999  iccdili  10001  icccntri  10003  fzprval  10084  fzofzp1  10229  fzostep1  10239  flqge0nn0  10295  flqge1nn  10296  fldiv4p1lem1div2  10307  exp1  10528  qexpclz  10543  nn0sqcl  10549  expeq0  10553  expubnd  10579  sqval  10580  sqeq0  10585  resqcl  10590  zsqcl  10593  iexpcyc  10627  binom21  10635  bcnn  10739  bcn2  10746  bcn2p1  10752  bcnm1  10754  fihasheq0  10775  hashsng  10780  fihashen1  10781  fimaxq  10809  shftfibg  10831  shftfib  10834  reim0  10872  imval2  10905  cjap0  10918  cjne0  10919  rexuz3  11001  resqrexlemover  11021  abssq  11092  nn0abscl  11096  nnabscl  11111  abs2dif  11117  max0addsup  11230  climshft  11314  bcxmas  11499  efgt1p2  11705  efgt1p  11706  efi4p  11727  resin4p  11728  recos4p  11729  sinbnd  11762  cosbnd  11763  dvdsval2  11799  zdvdsdc  11821  dvdsmul2  11823  dvdsmulcr  11830  dvdsabseq  11855  divconjdvds  11857  alzdvds  11862  fzo0dvdseq  11865  odd2np1lem  11879  mod2eq1n2dvds  11886  flodddiv4  11941  flodddiv4t2lthalf  11944  gcdmndc  11947  gcd0id  11982  gcd1  11990  dfgcd2  12017  gcdmultiple  12023  gcdmultiplez  12024  dvdssq  12034  lcmmndc  12064  lcm0val  12067  dvdslcm  12071  lcmeq0  12073  lcmgcd  12080  lcmdvds  12081  lcmid  12082  lcm1  12083  cncongr2  12106  isprm3  12120  prm2orodd  12128  sqrt2irrap  12182  phiprm  12225  pc0  12306  pcdvdstr  12328  unennn  12400  ennnfonelemim  12427  ctinfom  12431  ctinf  12433  enctlem  12435  elrestr  12701  tgval  12716  tgvalex  12717  xpsfrnel  12768  xpsfeq  12769  xpscf  12771  mulg1  12995  mulgnegnn  12998  subrgintm  13369  0opn  13545  topopn  13547  0cld  13651  ntropn  13656  ntrtop  13667  ntr0  13673  neipsm  13693  rest0  13718  xmetres  13921  metres  13922  mopnex  14044  tgioo  14085  cnlimcim  14179  cnlimc  14180  dvfre  14213  dveflem  14226  dvef  14227  efcn  14228  sin2pim  14273  cos2pim  14274  sinmpi  14275  cosmpi  14276  sinppi  14277  cosppi  14278  efimpi  14279  sincosq1lem  14285  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  sinq12gt0  14290  sinq34lt0t  14291  sincosq1eq  14299  abssinper  14306  logrpap0b  14336  loglt1b  14353  rpcxp0  14358  rpcxp1  14359  rpcxpsqrt  14381  logsqrt  14382  rprelogbdiv  14414  lgs0  14453  lgs2  14457  lgsneg  14464  lgsdilem  14467  lgsdir2lem2  14469  lgsdir2lem4  14471  lgsdir2lem5  14472  lgsne0  14478  bj-inf2vnlem1  14761  pwle2  14787  pwf1oexmid  14788  nninfsellemeqinf  14804  sbthom  14813  iswomninnlem  14836  redc0  14844