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  10472  fzostep1  10483  flqge0nn0  10553  flqge1nn  10554  fldiv4p1lem1div2  10565  exp1  10807  qexpclz  10822  nn0sqcl  10828  expeq0  10832  expubnd  10858  sqval  10859  sqeq0  10864  resqcl  10869  zsqcl  10872  iexpcyc  10906  binom21  10914  bcnn  11019  bcn2  11026  bcn2p1  11032  bcnm1  11034  fihasheq0  11055  hashsng  11060  fihashen1  11061  fimaxq  11091  iswrddm0  11137  ccatval2  11175  ccatsymb  11179  ccatrid  11184  eqs1  11205  s111  11208  swrdnd  11240  pfx00g  11256  shftfibg  11381  shftfib  11384  reim0  11422  imval2  11455  cjap0  11468  cjne0  11469  rexuz3  11551  resqrexlemover  11571  abssq  11642  nn0abscl  11646  nnabscl  11661  abs2dif  11667  max0addsup  11780  climshft  11865  bcxmas  12051  efgt1p2  12257  efgt1p  12258  efi4p  12279  resin4p  12280  recos4p  12281  sinbnd  12314  cosbnd  12315  dvdsval2  12352  zdvdsdc  12374  dvdsmul2  12376  dvdsmulcr  12383  dvdsabseq  12409  divconjdvds  12411  alzdvds  12416  fzo0dvdseq  12419  odd2np1lem  12434  mod2eq1n2dvds  12441  flodddiv4  12498  flodddiv4t2lthalf  12501  bits0  12510  bitsp1o  12515  gcdmndc  12527  gcd0id  12551  gcd1  12559  dfgcd2  12586  gcdmultiple  12592  gcdmultiplez  12593  dvdssq  12603  lcmmndc  12635  lcm0val  12638  dvdslcm  12642  lcmeq0  12644  lcmgcd  12651  lcmdvds  12652  lcmid  12653  lcm1  12654  cncongr2  12677  isprm3  12691  prm2orodd  12699  sqrt2irrap  12753  phiprm  12796  pc0  12878  pcxqcl  12886  pcdvdstr  12901  unennn  13019  ennnfonelemim  13046  ctinfom  13050  ctinf  13052  enctlem  13054  elrestr  13331  tgval  13346  tgvalex  13347  xpsfrnel  13428  xpsfeq  13429  xpscf  13431  mulg1  13717  mulgnegnn  13720  ghmghmrn  13851  subrngintm  14228  subrgintm  14259  lsp0  14439  mulgrhm2  14626  zlmlemg  14644  zlmsca  14648  0opn  14732  topopn  14734  0cld  14838  ntropn  14843  ntrtop  14854  ntr0  14860  neipsm  14880  rest0  14905  xmetres  15108  metres  15109  mopnex  15231  tgioo  15280  cnlimcim  15397  cnlimc  15398  dvfre  15436  dveflem  15452  dvef  15453  efcn  15494  sin2pim  15539  cos2pim  15540  sinmpi  15541  cosmpi  15542  sinppi  15543  cosppi  15544  efimpi  15545  sincosq1lem  15551  sincosq2sgn  15553  sincosq3sgn  15554  sincosq4sgn  15555  sinq12gt0  15556  sinq34lt0t  15557  sincosq1eq  15565  abssinper  15572  logrpap0b  15602  loglt1b  15619  rpcxp0  15624  rpcxp1  15625  rpcxpsqrt  15648  logsqrt  15649  rprelogbdiv  15683  lgs0  15744  lgs2  15748  lgsneg  15755  lgsdilem  15758  lgsdir2lem2  15760  lgsdir2lem4  15762  lgsdir2lem5  15763  lgsne0  15769  2lgslem1a2  15818  2lgslem1c  15821  upgr0eop  15975  uspgrushgr  16033  usgruspgr  16036  usgr0eop  16095  0grsubgr  16117  wlklenvclwlk  16226  upgr2wlkdc  16230  clwwlk0on0  16284  bj-inf2vnlem1  16568  pwle2  16602  pwf1oexmid  16603  domomsubct  16605  nninfsellemeqinf  16621  sbthom  16633  iswomninnlem  16656  redc0  16664