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  1365  equs4  1773  sb4bor  1883  elvd  2807  eueq2dc  2979  sbcgf  3099  csbconstgf  3140  sbcnestg  3181  csbnestg  3182  csbnest1g  3183  ssindif0im  3554  mpteq1  4173  iinexgm  4244  exmid1stab  4298  mss  4318  eusv2nf  4553  eldifpw  4574  ordtriexmid  4619  onsucsssucexmid  4625  ordsucunielexmid  4629  nn0suc  4702  xpss1  4836  xpiindim  4867  reldm0  4949  elrnmpt1s  4982  resdm  5052  resid  5070  eliniseg  5106  trinxp  5130  inimasn  5154  ssrnres  5179  cnveq0  5193  coi2  5253  relrelss  5263  funcnvres  5403  funimaex  5415  fnresin1  5447  fnresin2  5448  fresin  5515  dffv3g  5635  ssimaex  5707  dmfco  5714  fvmpt  5723  fsn  5819  fsn2  5821  funop  5831  elabrex  5898  elabrexg  5899  f1elima  5914  2ndconst  6387  tposfun  6426  tpostpos2  6431  tfrexlem  6500  tfri3  6533  rdgruledefgg  6541  rdgss  6549  frecsuclem  6572  frecrdg  6574  oa0  6625  om0  6626  oei0  6627  oav2  6631  oa1suc  6635  nnmsucr  6656  nnm1  6693  nnm2  6694  ecelqsg  6757  ecidg  6768  xpider  6775  qsel  6781  mapdm0  6832  map0e  6855  mapsnconst  6863  ixpsnf1o  6905  map1  6987  dom1o  7002  xp1en  7007  xpcomco  7010  xpmapenlem  7035  findcard2s  7079  findcard2d  7080  findcard2sd  7081  exmidpw  7100  residfi  7139  fidcenumlemr  7154  sbthlem7  7162  eqinfti  7219  djueq1  7239  omp1eomlem  7293  endjusym  7295  eninl  7296  eninr  7297  difinfsn  7299  finomni  7339  pm54.43  7395  exmidonfinlem  7404  2onetap  7474  mulidpi  7538  nlt1pig  7561  indpi  7562  halfnqq  7630  archnqq  7637  prarloclemarch  7638  prarloclemarch2  7639  nnnq  7642  nq0a0  7677  addpinq1  7684  prarloclemlt  7713  prarloclemlo  7714  prarloclem3  7717  prarloclemcalc  7722  nqprm  7762  addnqpr1  7782  1idprl  7810  1idpru  7811  1idpr  7812  recexprlem1ssl  7853  recexprlem1ssu  7854  ltmprr  7862  0idsr  7987  1idsr  7988  00sr  7989  pn0sr  7991  negexsr  7992  recexgt0sr  7993  ltm1sr  7997  archsr  8002  prsrcl  8004  prsradd  8006  mappsrprg  8024  map2psrprg  8025  elrealeu  8049  pitonnlem1p1  8066  peano2nnnn  8073  ax1rid  8097  axcnre  8101  peano5nnnn  8112  peano2cn  8314  peano2re  8315  addlid  8318  subid  8398  subid1  8399  negid  8426  negeq0  8433  peano2cnm  8445  peano2rem  8446  mul01  8568  lt0neg1  8648  le0neg1  8650  recexre  8758  inelr  8764  rimul  8765  reapmul1  8775  apsqgt0  8781  mulge0  8799  negap0  8810  divvalap  8854  rerecclap  8910  div2negap  8915  divgt0i2i  9097  peano5nni  9146  nnge1  9166  times2  9272  addltmul  9381  nn0p1nn  9441  peano2nn0  9442  nn0lele2xi  9453  znnnlt1  9527  nn0lt10b  9560  prime  9579  msqznn  9580  zeo  9585  elnn1uz2  9841  qreccl  9876  qdivcl  9877  irrmul  9881  rphalfcl  9916  rpnegap  9921  zgt1rpn0n1  9930  ltpnf  10015  nltmnf  10023  pnfge  10024  xlt0neg1  10073  xle0neg1  10075  xaddpnf1  10081  xaddmnf1  10083  xaddid1  10097  xsubge0  10116  xleaddadd  10122  elioopnf  10202  elicopnf  10204  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  fzprval  10317  fzofzp1  10473  fzostep1  10484  flqge0nn0  10554  flqge1nn  10555  fldiv4p1lem1div2  10566  exp1  10808  qexpclz  10823  nn0sqcl  10829  expeq0  10833  expubnd  10859  sqval  10860  sqeq0  10865  resqcl  10870  zsqcl  10873  iexpcyc  10907  binom21  10915  bcnn  11020  bcn2  11027  bcn2p1  11033  bcnm1  11035  fihasheq0  11056  hashsng  11061  fihashen1  11062  fimaxq  11092  iswrddm0  11141  ccatval2  11179  ccatsymb  11183  ccatrid  11188  eqs1  11209  s111  11212  swrdnd  11244  pfx00g  11260  shftfibg  11398  shftfib  11401  reim0  11439  imval2  11472  cjap0  11485  cjne0  11486  rexuz3  11568  resqrexlemover  11588  abssq  11659  nn0abscl  11663  nnabscl  11678  abs2dif  11684  max0addsup  11797  climshft  11882  bcxmas  12068  efgt1p2  12274  efgt1p  12275  efi4p  12296  resin4p  12297  recos4p  12298  sinbnd  12331  cosbnd  12332  dvdsval2  12369  zdvdsdc  12391  dvdsmul2  12393  dvdsmulcr  12400  dvdsabseq  12426  divconjdvds  12428  alzdvds  12433  fzo0dvdseq  12436  odd2np1lem  12451  mod2eq1n2dvds  12458  flodddiv4  12515  flodddiv4t2lthalf  12518  bits0  12527  bitsp1o  12532  gcdmndc  12544  gcd0id  12568  gcd1  12576  dfgcd2  12603  gcdmultiple  12609  gcdmultiplez  12610  dvdssq  12620  lcmmndc  12652  lcm0val  12655  dvdslcm  12659  lcmeq0  12661  lcmgcd  12668  lcmdvds  12669  lcmid  12670  lcm1  12671  cncongr2  12694  isprm3  12708  prm2orodd  12716  sqrt2irrap  12770  phiprm  12813  pc0  12895  pcxqcl  12903  pcdvdstr  12918  unennn  13036  ennnfonelemim  13063  ctinfom  13067  ctinf  13069  enctlem  13071  elrestr  13348  tgval  13363  tgvalex  13364  xpsfrnel  13445  xpsfeq  13446  xpscf  13448  mulg1  13734  mulgnegnn  13737  ghmghmrn  13868  subrngintm  14245  subrgintm  14276  lsp0  14456  mulgrhm2  14643  zlmlemg  14661  zlmsca  14665  0opn  14749  topopn  14751  0cld  14855  ntropn  14860  ntrtop  14871  ntr0  14877  neipsm  14897  rest0  14922  xmetres  15125  metres  15126  mopnex  15248  tgioo  15297  cnlimcim  15414  cnlimc  15415  dvfre  15453  dveflem  15469  dvef  15470  efcn  15511  sin2pim  15556  cos2pim  15557  sinmpi  15558  cosmpi  15559  sinppi  15560  cosppi  15561  efimpi  15562  sincosq1lem  15568  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  sinq34lt0t  15574  sincosq1eq  15582  abssinper  15589  logrpap0b  15619  loglt1b  15636  rpcxp0  15641  rpcxp1  15642  rpcxpsqrt  15665  logsqrt  15666  rprelogbdiv  15700  lgs0  15761  lgs2  15765  lgsneg  15772  lgsdilem  15775  lgsdir2lem2  15777  lgsdir2lem4  15779  lgsdir2lem5  15780  lgsne0  15786  2lgslem1a2  15835  2lgslem1c  15838  upgr0eop  15992  uspgrushgr  16050  usgruspgr  16053  usgr0eop  16112  0grsubgr  16134  wlklenvclwlk  16243  upgr2wlkdc  16247  clwwlk0on0  16301  konigsbergssiedgwen  16356  bj-inf2vnlem1  16616  pwle2  16650  pwf1oexmid  16651  domomsubct  16653  nninfsellemeqinf  16669  sbthom  16681  qdiff  16704  iswomninnlem  16705  redc0  16713