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  5830  elabrex  5897  elabrexg  5898  f1elima  5913  2ndconst  6386  tposfun  6425  tpostpos2  6430  tfrexlem  6499  tfri3  6532  rdgruledefgg  6540  rdgss  6548  frecsuclem  6571  frecrdg  6573  oa0  6624  om0  6625  oei0  6626  oav2  6630  oa1suc  6634  nnmsucr  6655  nnm1  6692  nnm2  6693  ecelqsg  6756  ecidg  6767  xpider  6774  qsel  6780  mapdm0  6831  map0e  6854  mapsnconst  6862  ixpsnf1o  6904  map1  6986  dom1o  7001  xp1en  7006  xpcomco  7009  xpmapenlem  7034  findcard2s  7078  findcard2d  7079  findcard2sd  7080  exmidpw  7099  residfi  7138  fidcenumlemr  7153  sbthlem7  7161  eqinfti  7218  djueq1  7238  omp1eomlem  7292  endjusym  7294  eninl  7295  eninr  7296  difinfsn  7298  finomni  7338  pm54.43  7394  exmidonfinlem  7403  2onetap  7473  mulidpi  7537  nlt1pig  7560  indpi  7561  halfnqq  7629  archnqq  7636  prarloclemarch  7637  prarloclemarch2  7638  nnnq  7641  nq0a0  7676  addpinq1  7683  prarloclemlt  7712  prarloclemlo  7713  prarloclem3  7716  prarloclemcalc  7721  nqprm  7761  addnqpr1  7781  1idprl  7809  1idpru  7810  1idpr  7811  recexprlem1ssl  7852  recexprlem1ssu  7853  ltmprr  7861  0idsr  7986  1idsr  7987  00sr  7988  pn0sr  7990  negexsr  7991  recexgt0sr  7992  ltm1sr  7996  archsr  8001  prsrcl  8003  prsradd  8005  mappsrprg  8023  map2psrprg  8024  elrealeu  8048  pitonnlem1p1  8065  peano2nnnn  8072  ax1rid  8096  axcnre  8100  peano5nnnn  8111  peano2cn  8313  peano2re  8314  addlid  8317  subid  8397  subid1  8398  negid  8425  negeq0  8432  peano2cnm  8444  peano2rem  8445  mul01  8567  lt0neg1  8647  le0neg1  8649  recexre  8757  inelr  8763  rimul  8764  reapmul1  8774  apsqgt0  8780  mulge0  8798  negap0  8809  divvalap  8853  rerecclap  8909  div2negap  8914  divgt0i2i  9096  peano5nni  9145  nnge1  9165  times2  9271  addltmul  9380  nn0p1nn  9440  peano2nn0  9441  nn0lele2xi  9452  znnnlt1  9526  nn0lt10b  9559  prime  9578  msqznn  9579  zeo  9584  elnn1uz2  9840  qreccl  9875  qdivcl  9876  irrmul  9880  rphalfcl  9915  rpnegap  9920  zgt1rpn0n1  9929  ltpnf  10014  nltmnf  10022  pnfge  10023  xlt0neg1  10072  xle0neg1  10074  xaddpnf1  10080  xaddmnf1  10082  xaddid1  10096  xsubge0  10115  xleaddadd  10121  elioopnf  10201  elicopnf  10203  iccshftri  10229  iccshftli  10231  iccdili  10233  icccntri  10235  fzprval  10316  fzofzp1  10471  fzostep1  10482  flqge0nn0  10552  flqge1nn  10553  fldiv4p1lem1div2  10564  exp1  10806  qexpclz  10821  nn0sqcl  10827  expeq0  10831  expubnd  10857  sqval  10858  sqeq0  10863  resqcl  10868  zsqcl  10871  iexpcyc  10905  binom21  10913  bcnn  11018  bcn2  11025  bcn2p1  11031  bcnm1  11033  fihasheq0  11054  hashsng  11059  fihashen1  11060  fimaxq  11090  iswrddm0  11136  ccatval2  11174  ccatsymb  11178  ccatrid  11183  eqs1  11204  s111  11207  swrdnd  11239  pfx00g  11255  shftfibg  11380  shftfib  11383  reim0  11421  imval2  11454  cjap0  11467  cjne0  11468  rexuz3  11550  resqrexlemover  11570  abssq  11641  nn0abscl  11645  nnabscl  11660  abs2dif  11666  max0addsup  11779  climshft  11864  bcxmas  12049  efgt1p2  12255  efgt1p  12256  efi4p  12277  resin4p  12278  recos4p  12279  sinbnd  12312  cosbnd  12313  dvdsval2  12350  zdvdsdc  12372  dvdsmul2  12374  dvdsmulcr  12381  dvdsabseq  12407  divconjdvds  12409  alzdvds  12414  fzo0dvdseq  12417  odd2np1lem  12432  mod2eq1n2dvds  12439  flodddiv4  12496  flodddiv4t2lthalf  12499  bits0  12508  bitsp1o  12513  gcdmndc  12525  gcd0id  12549  gcd1  12557  dfgcd2  12584  gcdmultiple  12590  gcdmultiplez  12591  dvdssq  12601  lcmmndc  12633  lcm0val  12636  dvdslcm  12640  lcmeq0  12642  lcmgcd  12649  lcmdvds  12650  lcmid  12651  lcm1  12652  cncongr2  12675  isprm3  12689  prm2orodd  12697  sqrt2irrap  12751  phiprm  12794  pc0  12876  pcxqcl  12884  pcdvdstr  12899  unennn  13017  ennnfonelemim  13044  ctinfom  13048  ctinf  13050  enctlem  13052  elrestr  13329  tgval  13344  tgvalex  13345  xpsfrnel  13426  xpsfeq  13427  xpscf  13429  mulg1  13715  mulgnegnn  13718  ghmghmrn  13849  subrngintm  14225  subrgintm  14256  lsp0  14436  mulgrhm2  14623  zlmlemg  14641  zlmsca  14645  0opn  14729  topopn  14731  0cld  14835  ntropn  14840  ntrtop  14851  ntr0  14857  neipsm  14877  rest0  14902  xmetres  15105  metres  15106  mopnex  15228  tgioo  15277  cnlimcim  15394  cnlimc  15395  dvfre  15433  dveflem  15449  dvef  15450  efcn  15491  sin2pim  15536  cos2pim  15537  sinmpi  15538  cosmpi  15539  sinppi  15540  cosppi  15541  efimpi  15542  sincosq1lem  15548  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  sinq34lt0t  15554  sincosq1eq  15562  abssinper  15569  logrpap0b  15599  loglt1b  15616  rpcxp0  15621  rpcxp1  15622  rpcxpsqrt  15645  logsqrt  15646  rprelogbdiv  15680  lgs0  15741  lgs2  15745  lgsneg  15752  lgsdilem  15755  lgsdir2lem2  15757  lgsdir2lem4  15759  lgsdir2lem5  15760  lgsne0  15766  2lgslem1a2  15815  2lgslem1c  15818  upgr0eop  15972  uspgrushgr  16030  usgruspgr  16033  usgr0eop  16092  0grsubgr  16114  wlklenvclwlk  16223  upgr2wlkdc  16227  clwwlk0on0  16281  bj-inf2vnlem1  16565  pwle2  16599  pwf1oexmid  16600  domomsubct  16602  nninfsellemeqinf  16618  sbthom  16630  iswomninnlem  16653  redc0  16661