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  1340  equs4  1739  sb4bor  1849  elvd  2768  eueq2dc  2937  sbcgf  3057  csbconstgf  3097  sbcnestg  3138  csbnestg  3139  csbnest1g  3140  ssindif0im  3510  mpteq1  4117  iinexgm  4187  exmid1stab  4241  mss  4259  eusv2nf  4491  eldifpw  4512  ordtriexmid  4557  onsucsssucexmid  4563  ordsucunielexmid  4567  nn0suc  4640  xpss1  4773  xpiindim  4803  reldm0  4884  elrnmpt1s  4916  resdm  4985  resid  5003  eliniseg  5039  trinxp  5063  inimasn  5087  ssrnres  5112  cnveq0  5126  coi2  5186  relrelss  5196  funcnvres  5331  funimaex  5343  fnresin1  5372  fnresin2  5373  fresin  5436  dffv3g  5554  ssimaex  5622  dmfco  5629  fvmpt  5638  fsn  5734  fsn2  5736  elabrex  5804  elabrexg  5805  f1elima  5820  2ndconst  6280  tposfun  6318  tpostpos2  6323  tfrexlem  6392  tfri3  6425  rdgruledefgg  6433  rdgss  6441  frecsuclem  6464  frecrdg  6466  oa0  6515  om0  6516  oei0  6517  oav2  6521  oa1suc  6525  nnmsucr  6546  nnm1  6583  nnm2  6584  ecelqsg  6647  ecidg  6658  xpider  6665  qsel  6671  mapdm0  6722  map0e  6745  mapsnconst  6753  ixpsnf1o  6795  map1  6871  xp1en  6882  xpcomco  6885  xpmapenlem  6910  findcard2s  6951  findcard2d  6952  findcard2sd  6953  exmidpw  6969  residfi  7006  fidcenumlemr  7021  sbthlem7  7029  eqinfti  7086  djueq1  7106  omp1eomlem  7160  endjusym  7162  eninl  7163  eninr  7164  difinfsn  7166  finomni  7206  pm54.43  7257  exmidonfinlem  7260  2onetap  7322  mulidpi  7385  nlt1pig  7408  indpi  7409  halfnqq  7477  archnqq  7484  prarloclemarch  7485  prarloclemarch2  7486  nnnq  7489  nq0a0  7524  addpinq1  7531  prarloclemlt  7560  prarloclemlo  7561  prarloclem3  7564  prarloclemcalc  7569  nqprm  7609  addnqpr1  7629  1idprl  7657  1idpru  7658  1idpr  7659  recexprlem1ssl  7700  recexprlem1ssu  7701  ltmprr  7709  0idsr  7834  1idsr  7835  00sr  7836  pn0sr  7838  negexsr  7839  recexgt0sr  7840  ltm1sr  7844  archsr  7849  prsrcl  7851  prsradd  7853  mappsrprg  7871  map2psrprg  7872  elrealeu  7896  pitonnlem1p1  7913  peano2nnnn  7920  ax1rid  7944  axcnre  7948  peano5nnnn  7959  peano2cn  8161  peano2re  8162  addlid  8165  subid  8245  subid1  8246  negid  8273  negeq0  8280  peano2cnm  8292  peano2rem  8293  mul01  8415  lt0neg1  8495  le0neg1  8497  recexre  8605  inelr  8611  rimul  8612  reapmul1  8622  apsqgt0  8628  mulge0  8646  negap0  8657  divvalap  8701  rerecclap  8757  div2negap  8762  divgt0i2i  8944  peano5nni  8993  nnge1  9013  times2  9119  addltmul  9228  nn0p1nn  9288  peano2nn0  9289  nn0lele2xi  9300  znnnlt1  9374  nn0lt10b  9406  prime  9425  msqznn  9426  zeo  9431  elnn1uz2  9681  qreccl  9716  qdivcl  9717  irrmul  9721  rphalfcl  9756  rpnegap  9761  zgt1rpn0n1  9770  ltpnf  9855  nltmnf  9863  pnfge  9864  xlt0neg1  9913  xle0neg1  9915  xaddpnf1  9921  xaddmnf1  9923  xaddid1  9937  xsubge0  9956  xleaddadd  9962  elioopnf  10042  elicopnf  10044  iccshftri  10070  iccshftli  10072  iccdili  10074  icccntri  10076  fzprval  10157  fzofzp1  10303  fzostep1  10313  flqge0nn0  10383  flqge1nn  10384  fldiv4p1lem1div2  10395  exp1  10637  qexpclz  10652  nn0sqcl  10658  expeq0  10662  expubnd  10688  sqval  10689  sqeq0  10694  resqcl  10699  zsqcl  10702  iexpcyc  10736  binom21  10744  bcnn  10849  bcn2  10856  bcn2p1  10862  bcnm1  10864  fihasheq0  10885  hashsng  10890  fihashen1  10891  fimaxq  10919  iswrddm0  10959  shftfibg  10985  shftfib  10988  reim0  11026  imval2  11059  cjap0  11072  cjne0  11073  rexuz3  11155  resqrexlemover  11175  abssq  11246  nn0abscl  11250  nnabscl  11265  abs2dif  11271  max0addsup  11384  climshft  11469  bcxmas  11654  efgt1p2  11860  efgt1p  11861  efi4p  11882  resin4p  11883  recos4p  11884  sinbnd  11917  cosbnd  11918  dvdsval2  11955  zdvdsdc  11977  dvdsmul2  11979  dvdsmulcr  11986  dvdsabseq  12012  divconjdvds  12014  alzdvds  12019  fzo0dvdseq  12022  odd2np1lem  12037  mod2eq1n2dvds  12044  flodddiv4  12101  flodddiv4t2lthalf  12104  bits0  12112  bitsp1o  12117  gcdmndc  12122  gcd0id  12146  gcd1  12154  dfgcd2  12181  gcdmultiple  12187  gcdmultiplez  12188  dvdssq  12198  lcmmndc  12230  lcm0val  12233  dvdslcm  12237  lcmeq0  12239  lcmgcd  12246  lcmdvds  12247  lcmid  12248  lcm1  12249  cncongr2  12272  isprm3  12286  prm2orodd  12294  sqrt2irrap  12348  phiprm  12391  pc0  12473  pcxqcl  12481  pcdvdstr  12496  unennn  12614  ennnfonelemim  12641  ctinfom  12645  ctinf  12647  enctlem  12649  elrestr  12918  tgval  12933  tgvalex  12934  xpsfrnel  12987  xpsfeq  12988  xpscf  12990  mulg1  13259  mulgnegnn  13262  ghmghmrn  13393  subrngintm  13768  subrgintm  13799  lsp0  13979  mulgrhm2  14166  zlmlemg  14184  zlmsca  14188  0opn  14242  topopn  14244  0cld  14348  ntropn  14353  ntrtop  14364  ntr0  14370  neipsm  14390  rest0  14415  xmetres  14618  metres  14619  mopnex  14741  tgioo  14790  cnlimcim  14907  cnlimc  14908  dvfre  14946  dveflem  14962  dvef  14963  efcn  15004  sin2pim  15049  cos2pim  15050  sinmpi  15051  cosmpi  15052  sinppi  15053  cosppi  15054  efimpi  15055  sincosq1lem  15061  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  sinq34lt0t  15067  sincosq1eq  15075  abssinper  15082  logrpap0b  15112  loglt1b  15129  rpcxp0  15134  rpcxp1  15135  rpcxpsqrt  15158  logsqrt  15159  rprelogbdiv  15193  lgs0  15254  lgs2  15258  lgsneg  15265  lgsdilem  15268  lgsdir2lem2  15270  lgsdir2lem4  15272  lgsdir2lem5  15273  lgsne0  15279  2lgslem1a2  15328  2lgslem1c  15331  bj-inf2vnlem1  15616  pwle2  15643  pwf1oexmid  15644  nninfsellemeqinf  15660  sbthom  15670  iswomninnlem  15693  redc0  15701