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  1342  equs4  1748  sb4bor  1858  elvd  2777  eueq2dc  2946  sbcgf  3066  csbconstgf  3106  sbcnestg  3147  csbnestg  3148  csbnest1g  3149  ssindif0im  3520  mpteq1  4129  iinexgm  4199  exmid1stab  4253  mss  4271  eusv2nf  4504  eldifpw  4525  ordtriexmid  4570  onsucsssucexmid  4576  ordsucunielexmid  4580  nn0suc  4653  xpss1  4786  xpiindim  4816  reldm0  4897  elrnmpt1s  4929  resdm  4999  resid  5017  eliniseg  5053  trinxp  5077  inimasn  5101  ssrnres  5126  cnveq0  5140  coi2  5200  relrelss  5210  funcnvres  5348  funimaex  5360  fnresin1  5392  fnresin2  5393  fresin  5456  dffv3g  5574  ssimaex  5642  dmfco  5649  fvmpt  5658  fsn  5754  fsn2  5756  funop  5765  elabrex  5828  elabrexg  5829  f1elima  5844  2ndconst  6310  tposfun  6348  tpostpos2  6353  tfrexlem  6422  tfri3  6455  rdgruledefgg  6463  rdgss  6471  frecsuclem  6494  frecrdg  6496  oa0  6545  om0  6546  oei0  6547  oav2  6551  oa1suc  6555  nnmsucr  6576  nnm1  6613  nnm2  6614  ecelqsg  6677  ecidg  6688  xpider  6695  qsel  6701  mapdm0  6752  map0e  6775  mapsnconst  6783  ixpsnf1o  6825  map1  6906  xp1en  6920  xpcomco  6923  xpmapenlem  6948  findcard2s  6989  findcard2d  6990  findcard2sd  6991  exmidpw  7007  residfi  7044  fidcenumlemr  7059  sbthlem7  7067  eqinfti  7124  djueq1  7144  omp1eomlem  7198  endjusym  7200  eninl  7201  eninr  7202  difinfsn  7204  finomni  7244  pm54.43  7300  exmidonfinlem  7303  2onetap  7369  mulidpi  7433  nlt1pig  7456  indpi  7457  halfnqq  7525  archnqq  7532  prarloclemarch  7533  prarloclemarch2  7534  nnnq  7537  nq0a0  7572  addpinq1  7579  prarloclemlt  7608  prarloclemlo  7609  prarloclem3  7612  prarloclemcalc  7617  nqprm  7657  addnqpr1  7677  1idprl  7705  1idpru  7706  1idpr  7707  recexprlem1ssl  7748  recexprlem1ssu  7749  ltmprr  7757  0idsr  7882  1idsr  7883  00sr  7884  pn0sr  7886  negexsr  7887  recexgt0sr  7888  ltm1sr  7892  archsr  7897  prsrcl  7899  prsradd  7901  mappsrprg  7919  map2psrprg  7920  elrealeu  7944  pitonnlem1p1  7961  peano2nnnn  7968  ax1rid  7992  axcnre  7996  peano5nnnn  8007  peano2cn  8209  peano2re  8210  addlid  8213  subid  8293  subid1  8294  negid  8321  negeq0  8328  peano2cnm  8340  peano2rem  8341  mul01  8463  lt0neg1  8543  le0neg1  8545  recexre  8653  inelr  8659  rimul  8660  reapmul1  8670  apsqgt0  8676  mulge0  8694  negap0  8705  divvalap  8749  rerecclap  8805  div2negap  8810  divgt0i2i  8992  peano5nni  9041  nnge1  9061  times2  9167  addltmul  9276  nn0p1nn  9336  peano2nn0  9337  nn0lele2xi  9348  znnnlt1  9422  nn0lt10b  9455  prime  9474  msqznn  9475  zeo  9480  elnn1uz2  9730  qreccl  9765  qdivcl  9766  irrmul  9770  rphalfcl  9805  rpnegap  9810  zgt1rpn0n1  9819  ltpnf  9904  nltmnf  9912  pnfge  9913  xlt0neg1  9962  xle0neg1  9964  xaddpnf1  9970  xaddmnf1  9972  xaddid1  9986  xsubge0  10005  xleaddadd  10011  elioopnf  10091  elicopnf  10093  iccshftri  10119  iccshftli  10121  iccdili  10123  icccntri  10125  fzprval  10206  fzofzp1  10358  fzostep1  10368  flqge0nn0  10438  flqge1nn  10439  fldiv4p1lem1div2  10450  exp1  10692  qexpclz  10707  nn0sqcl  10713  expeq0  10717  expubnd  10743  sqval  10744  sqeq0  10749  resqcl  10754  zsqcl  10757  iexpcyc  10791  binom21  10799  bcnn  10904  bcn2  10911  bcn2p1  10917  bcnm1  10919  fihasheq0  10940  hashsng  10945  fihashen1  10946  fimaxq  10974  iswrddm0  11020  ccatval2  11057  ccatsymb  11061  ccatrid  11066  eqs1  11085  s111  11088  swrdnd  11115  pfx00g  11131  shftfibg  11164  shftfib  11167  reim0  11205  imval2  11238  cjap0  11251  cjne0  11252  rexuz3  11334  resqrexlemover  11354  abssq  11425  nn0abscl  11429  nnabscl  11444  abs2dif  11450  max0addsup  11563  climshft  11648  bcxmas  11833  efgt1p2  12039  efgt1p  12040  efi4p  12061  resin4p  12062  recos4p  12063  sinbnd  12096  cosbnd  12097  dvdsval2  12134  zdvdsdc  12156  dvdsmul2  12158  dvdsmulcr  12165  dvdsabseq  12191  divconjdvds  12193  alzdvds  12198  fzo0dvdseq  12201  odd2np1lem  12216  mod2eq1n2dvds  12223  flodddiv4  12280  flodddiv4t2lthalf  12283  bits0  12292  bitsp1o  12297  gcdmndc  12309  gcd0id  12333  gcd1  12341  dfgcd2  12368  gcdmultiple  12374  gcdmultiplez  12375  dvdssq  12385  lcmmndc  12417  lcm0val  12420  dvdslcm  12424  lcmeq0  12426  lcmgcd  12433  lcmdvds  12434  lcmid  12435  lcm1  12436  cncongr2  12459  isprm3  12473  prm2orodd  12481  sqrt2irrap  12535  phiprm  12578  pc0  12660  pcxqcl  12668  pcdvdstr  12683  unennn  12801  ennnfonelemim  12828  ctinfom  12832  ctinf  12834  enctlem  12836  elrestr  13112  tgval  13127  tgvalex  13128  xpsfrnel  13209  xpsfeq  13210  xpscf  13212  mulg1  13498  mulgnegnn  13501  ghmghmrn  13632  subrngintm  14007  subrgintm  14038  lsp0  14218  mulgrhm2  14405  zlmlemg  14423  zlmsca  14427  0opn  14511  topopn  14513  0cld  14617  ntropn  14622  ntrtop  14633  ntr0  14639  neipsm  14659  rest0  14684  xmetres  14887  metres  14888  mopnex  15010  tgioo  15059  cnlimcim  15176  cnlimc  15177  dvfre  15215  dveflem  15231  dvef  15232  efcn  15273  sin2pim  15318  cos2pim  15319  sinmpi  15320  cosmpi  15321  sinppi  15322  cosppi  15323  efimpi  15324  sincosq1lem  15330  sincosq2sgn  15332  sincosq3sgn  15333  sincosq4sgn  15334  sinq12gt0  15335  sinq34lt0t  15336  sincosq1eq  15344  abssinper  15351  logrpap0b  15381  loglt1b  15398  rpcxp0  15403  rpcxp1  15404  rpcxpsqrt  15427  logsqrt  15428  rprelogbdiv  15462  lgs0  15523  lgs2  15527  lgsneg  15534  lgsdilem  15537  lgsdir2lem2  15539  lgsdir2lem4  15541  lgsdir2lem5  15542  lgsne0  15548  2lgslem1a2  15597  2lgslem1c  15600  bj-inf2vnlem1  15943  pwle2  15972  pwf1oexmid  15973  domomsubct  15975  nninfsellemeqinf  15990  sbthom  16002  iswomninnlem  16025  redc0  16033