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  1749  sb4bor  1859  elvd  2781  eueq2dc  2953  sbcgf  3073  csbconstgf  3114  sbcnestg  3155  csbnestg  3156  csbnest1g  3157  ssindif0im  3528  mpteq1  4144  iinexgm  4214  exmid1stab  4268  mss  4288  eusv2nf  4521  eldifpw  4542  ordtriexmid  4587  onsucsssucexmid  4593  ordsucunielexmid  4597  nn0suc  4670  xpss1  4803  xpiindim  4833  reldm0  4915  elrnmpt1s  4947  resdm  5017  resid  5035  eliniseg  5071  trinxp  5095  inimasn  5119  ssrnres  5144  cnveq0  5158  coi2  5218  relrelss  5228  funcnvres  5366  funimaex  5378  fnresin1  5410  fnresin2  5411  fresin  5476  dffv3g  5595  ssimaex  5663  dmfco  5670  fvmpt  5679  fsn  5775  fsn2  5777  funop  5786  elabrex  5849  elabrexg  5850  f1elima  5865  2ndconst  6331  tposfun  6369  tpostpos2  6374  tfrexlem  6443  tfri3  6476  rdgruledefgg  6484  rdgss  6492  frecsuclem  6515  frecrdg  6517  oa0  6566  om0  6567  oei0  6568  oav2  6572  oa1suc  6576  nnmsucr  6597  nnm1  6634  nnm2  6635  ecelqsg  6698  ecidg  6709  xpider  6716  qsel  6722  mapdm0  6773  map0e  6796  mapsnconst  6804  ixpsnf1o  6846  map1  6928  xp1en  6943  xpcomco  6946  xpmapenlem  6971  findcard2s  7013  findcard2d  7014  findcard2sd  7015  exmidpw  7031  residfi  7068  fidcenumlemr  7083  sbthlem7  7091  eqinfti  7148  djueq1  7168  omp1eomlem  7222  endjusym  7224  eninl  7225  eninr  7226  difinfsn  7228  finomni  7268  pm54.43  7324  exmidonfinlem  7332  2onetap  7402  mulidpi  7466  nlt1pig  7489  indpi  7490  halfnqq  7558  archnqq  7565  prarloclemarch  7566  prarloclemarch2  7567  nnnq  7570  nq0a0  7605  addpinq1  7612  prarloclemlt  7641  prarloclemlo  7642  prarloclem3  7645  prarloclemcalc  7650  nqprm  7690  addnqpr1  7710  1idprl  7738  1idpru  7739  1idpr  7740  recexprlem1ssl  7781  recexprlem1ssu  7782  ltmprr  7790  0idsr  7915  1idsr  7916  00sr  7917  pn0sr  7919  negexsr  7920  recexgt0sr  7921  ltm1sr  7925  archsr  7930  prsrcl  7932  prsradd  7934  mappsrprg  7952  map2psrprg  7953  elrealeu  7977  pitonnlem1p1  7994  peano2nnnn  8001  ax1rid  8025  axcnre  8029  peano5nnnn  8040  peano2cn  8242  peano2re  8243  addlid  8246  subid  8326  subid1  8327  negid  8354  negeq0  8361  peano2cnm  8373  peano2rem  8374  mul01  8496  lt0neg1  8576  le0neg1  8578  recexre  8686  inelr  8692  rimul  8693  reapmul1  8703  apsqgt0  8709  mulge0  8727  negap0  8738  divvalap  8782  rerecclap  8838  div2negap  8843  divgt0i2i  9025  peano5nni  9074  nnge1  9094  times2  9200  addltmul  9309  nn0p1nn  9369  peano2nn0  9370  nn0lele2xi  9381  znnnlt1  9455  nn0lt10b  9488  prime  9507  msqznn  9508  zeo  9513  elnn1uz2  9763  qreccl  9798  qdivcl  9799  irrmul  9803  rphalfcl  9838  rpnegap  9843  zgt1rpn0n1  9852  ltpnf  9937  nltmnf  9945  pnfge  9946  xlt0neg1  9995  xle0neg1  9997  xaddpnf1  10003  xaddmnf1  10005  xaddid1  10019  xsubge0  10038  xleaddadd  10044  elioopnf  10124  elicopnf  10126  iccshftri  10152  iccshftli  10154  iccdili  10156  icccntri  10158  fzprval  10239  fzofzp1  10393  fzostep1  10403  flqge0nn0  10473  flqge1nn  10474  fldiv4p1lem1div2  10485  exp1  10727  qexpclz  10742  nn0sqcl  10748  expeq0  10752  expubnd  10778  sqval  10779  sqeq0  10784  resqcl  10789  zsqcl  10792  iexpcyc  10826  binom21  10834  bcnn  10939  bcn2  10946  bcn2p1  10952  bcnm1  10954  fihasheq0  10975  hashsng  10980  fihashen1  10981  fimaxq  11009  iswrddm0  11055  ccatval2  11092  ccatsymb  11096  ccatrid  11101  eqs1  11120  s111  11123  swrdnd  11150  pfx00g  11166  shftfibg  11246  shftfib  11249  reim0  11287  imval2  11320  cjap0  11333  cjne0  11334  rexuz3  11416  resqrexlemover  11436  abssq  11507  nn0abscl  11511  nnabscl  11526  abs2dif  11532  max0addsup  11645  climshft  11730  bcxmas  11915  efgt1p2  12121  efgt1p  12122  efi4p  12143  resin4p  12144  recos4p  12145  sinbnd  12178  cosbnd  12179  dvdsval2  12216  zdvdsdc  12238  dvdsmul2  12240  dvdsmulcr  12247  dvdsabseq  12273  divconjdvds  12275  alzdvds  12280  fzo0dvdseq  12283  odd2np1lem  12298  mod2eq1n2dvds  12305  flodddiv4  12362  flodddiv4t2lthalf  12365  bits0  12374  bitsp1o  12379  gcdmndc  12391  gcd0id  12415  gcd1  12423  dfgcd2  12450  gcdmultiple  12456  gcdmultiplez  12457  dvdssq  12467  lcmmndc  12499  lcm0val  12502  dvdslcm  12506  lcmeq0  12508  lcmgcd  12515  lcmdvds  12516  lcmid  12517  lcm1  12518  cncongr2  12541  isprm3  12555  prm2orodd  12563  sqrt2irrap  12617  phiprm  12660  pc0  12742  pcxqcl  12750  pcdvdstr  12765  unennn  12883  ennnfonelemim  12910  ctinfom  12914  ctinf  12916  enctlem  12918  elrestr  13194  tgval  13209  tgvalex  13210  xpsfrnel  13291  xpsfeq  13292  xpscf  13294  mulg1  13580  mulgnegnn  13583  ghmghmrn  13714  subrngintm  14089  subrgintm  14120  lsp0  14300  mulgrhm2  14487  zlmlemg  14505  zlmsca  14509  0opn  14593  topopn  14595  0cld  14699  ntropn  14704  ntrtop  14715  ntr0  14721  neipsm  14741  rest0  14766  xmetres  14969  metres  14970  mopnex  15092  tgioo  15141  cnlimcim  15258  cnlimc  15259  dvfre  15297  dveflem  15313  dvef  15314  efcn  15355  sin2pim  15400  cos2pim  15401  sinmpi  15402  cosmpi  15403  sinppi  15404  cosppi  15405  efimpi  15406  sincosq1lem  15412  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  sinq12gt0  15417  sinq34lt0t  15418  sincosq1eq  15426  abssinper  15433  logrpap0b  15463  loglt1b  15480  rpcxp0  15485  rpcxp1  15486  rpcxpsqrt  15509  logsqrt  15510  rprelogbdiv  15544  lgs0  15605  lgs2  15609  lgsneg  15616  lgsdilem  15619  lgsdir2lem2  15621  lgsdir2lem4  15623  lgsdir2lem5  15624  lgsne0  15630  2lgslem1a2  15679  2lgslem1c  15682  upgr0eop  15830  bj-inf2vnlem1  16105  dom1o  16128  pwle2  16137  pwf1oexmid  16138  domomsubct  16140  nninfsellemeqinf  16155  sbthom  16167  iswomninnlem  16190  redc0  16198