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  1363  equs4  1771  sb4bor  1881  elvd  2805  eueq2dc  2977  sbcgf  3097  csbconstgf  3138  sbcnestg  3179  csbnestg  3180  csbnest1g  3181  ssindif0im  3552  mpteq1  4171  iinexgm  4242  exmid1stab  4296  mss  4316  eusv2nf  4551  eldifpw  4572  ordtriexmid  4617  onsucsssucexmid  4623  ordsucunielexmid  4627  nn0suc  4700  xpss1  4834  xpiindim  4865  reldm0  4947  elrnmpt1s  4980  resdm  5050  resid  5068  eliniseg  5104  trinxp  5128  inimasn  5152  ssrnres  5177  cnveq0  5191  coi2  5251  relrelss  5261  funcnvres  5400  funimaex  5412  fnresin1  5444  fnresin2  5445  fresin  5512  dffv3g  5631  ssimaex  5703  dmfco  5710  fvmpt  5719  fsn  5815  fsn2  5817  funop  5826  elabrex  5893  elabrexg  5894  f1elima  5909  2ndconst  6382  tposfun  6421  tpostpos2  6426  tfrexlem  6495  tfri3  6528  rdgruledefgg  6536  rdgss  6544  frecsuclem  6567  frecrdg  6569  oa0  6620  om0  6621  oei0  6622  oav2  6626  oa1suc  6630  nnmsucr  6651  nnm1  6688  nnm2  6689  ecelqsg  6752  ecidg  6763  xpider  6770  qsel  6776  mapdm0  6827  map0e  6850  mapsnconst  6858  ixpsnf1o  6900  map1  6982  dom1o  6997  xp1en  7002  xpcomco  7005  xpmapenlem  7030  findcard2s  7072  findcard2d  7073  findcard2sd  7074  exmidpw  7093  residfi  7130  fidcenumlemr  7145  sbthlem7  7153  eqinfti  7210  djueq1  7230  omp1eomlem  7284  endjusym  7286  eninl  7287  eninr  7288  difinfsn  7290  finomni  7330  pm54.43  7386  exmidonfinlem  7394  2onetap  7464  mulidpi  7528  nlt1pig  7551  indpi  7552  halfnqq  7620  archnqq  7627  prarloclemarch  7628  prarloclemarch2  7629  nnnq  7632  nq0a0  7667  addpinq1  7674  prarloclemlt  7703  prarloclemlo  7704  prarloclem3  7707  prarloclemcalc  7712  nqprm  7752  addnqpr1  7772  1idprl  7800  1idpru  7801  1idpr  7802  recexprlem1ssl  7843  recexprlem1ssu  7844  ltmprr  7852  0idsr  7977  1idsr  7978  00sr  7979  pn0sr  7981  negexsr  7982  recexgt0sr  7983  ltm1sr  7987  archsr  7992  prsrcl  7994  prsradd  7996  mappsrprg  8014  map2psrprg  8015  elrealeu  8039  pitonnlem1p1  8056  peano2nnnn  8063  ax1rid  8087  axcnre  8091  peano5nnnn  8102  peano2cn  8304  peano2re  8305  addlid  8308  subid  8388  subid1  8389  negid  8416  negeq0  8423  peano2cnm  8435  peano2rem  8436  mul01  8558  lt0neg1  8638  le0neg1  8640  recexre  8748  inelr  8754  rimul  8755  reapmul1  8765  apsqgt0  8771  mulge0  8789  negap0  8800  divvalap  8844  rerecclap  8900  div2negap  8905  divgt0i2i  9087  peano5nni  9136  nnge1  9156  times2  9262  addltmul  9371  nn0p1nn  9431  peano2nn0  9432  nn0lele2xi  9443  znnnlt1  9517  nn0lt10b  9550  prime  9569  msqznn  9570  zeo  9575  elnn1uz2  9831  qreccl  9866  qdivcl  9867  irrmul  9871  rphalfcl  9906  rpnegap  9911  zgt1rpn0n1  9920  ltpnf  10005  nltmnf  10013  pnfge  10014  xlt0neg1  10063  xle0neg1  10065  xaddpnf1  10071  xaddmnf1  10073  xaddid1  10087  xsubge0  10106  xleaddadd  10112  elioopnf  10192  elicopnf  10194  iccshftri  10220  iccshftli  10222  iccdili  10224  icccntri  10226  fzprval  10307  fzofzp1  10462  fzostep1  10473  flqge0nn0  10543  flqge1nn  10544  fldiv4p1lem1div2  10555  exp1  10797  qexpclz  10812  nn0sqcl  10818  expeq0  10822  expubnd  10848  sqval  10849  sqeq0  10854  resqcl  10859  zsqcl  10862  iexpcyc  10896  binom21  10904  bcnn  11009  bcn2  11016  bcn2p1  11022  bcnm1  11024  fihasheq0  11045  hashsng  11050  fihashen1  11051  fimaxq  11081  iswrddm0  11127  ccatval2  11165  ccatsymb  11169  ccatrid  11174  eqs1  11195  s111  11198  swrdnd  11230  pfx00g  11246  shftfibg  11371  shftfib  11374  reim0  11412  imval2  11445  cjap0  11458  cjne0  11459  rexuz3  11541  resqrexlemover  11561  abssq  11632  nn0abscl  11636  nnabscl  11651  abs2dif  11657  max0addsup  11770  climshft  11855  bcxmas  12040  efgt1p2  12246  efgt1p  12247  efi4p  12268  resin4p  12269  recos4p  12270  sinbnd  12303  cosbnd  12304  dvdsval2  12341  zdvdsdc  12363  dvdsmul2  12365  dvdsmulcr  12372  dvdsabseq  12398  divconjdvds  12400  alzdvds  12405  fzo0dvdseq  12408  odd2np1lem  12423  mod2eq1n2dvds  12430  flodddiv4  12487  flodddiv4t2lthalf  12490  bits0  12499  bitsp1o  12504  gcdmndc  12516  gcd0id  12540  gcd1  12548  dfgcd2  12575  gcdmultiple  12581  gcdmultiplez  12582  dvdssq  12592  lcmmndc  12624  lcm0val  12627  dvdslcm  12631  lcmeq0  12633  lcmgcd  12640  lcmdvds  12641  lcmid  12642  lcm1  12643  cncongr2  12666  isprm3  12680  prm2orodd  12688  sqrt2irrap  12742  phiprm  12785  pc0  12867  pcxqcl  12875  pcdvdstr  12890  unennn  13008  ennnfonelemim  13035  ctinfom  13039  ctinf  13041  enctlem  13043  elrestr  13320  tgval  13335  tgvalex  13336  xpsfrnel  13417  xpsfeq  13418  xpscf  13420  mulg1  13706  mulgnegnn  13709  ghmghmrn  13840  subrngintm  14216  subrgintm  14247  lsp0  14427  mulgrhm2  14614  zlmlemg  14632  zlmsca  14636  0opn  14720  topopn  14722  0cld  14826  ntropn  14831  ntrtop  14842  ntr0  14848  neipsm  14868  rest0  14893  xmetres  15096  metres  15097  mopnex  15219  tgioo  15268  cnlimcim  15385  cnlimc  15386  dvfre  15424  dveflem  15440  dvef  15441  efcn  15482  sin2pim  15527  cos2pim  15528  sinmpi  15529  cosmpi  15530  sinppi  15531  cosppi  15532  efimpi  15533  sincosq1lem  15539  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  sinq34lt0t  15545  sincosq1eq  15553  abssinper  15560  logrpap0b  15590  loglt1b  15607  rpcxp0  15612  rpcxp1  15613  rpcxpsqrt  15636  logsqrt  15637  rprelogbdiv  15671  lgs0  15732  lgs2  15736  lgsneg  15743  lgsdilem  15746  lgsdir2lem2  15748  lgsdir2lem4  15750  lgsdir2lem5  15751  lgsne0  15757  2lgslem1a2  15806  2lgslem1c  15809  upgr0eop  15963  uspgrushgr  16019  usgruspgr  16022  usgr0eop  16081  wlklenvclwlk  16170  upgr2wlkdc  16172  clwwlk0on0  16226  bj-inf2vnlem1  16501  pwle2  16535  pwf1oexmid  16536  domomsubct  16538  nninfsellemeqinf  16554  sbthom  16566  iswomninnlem  16589  redc0  16597