Theorem mpan2 429

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 425	1 |- ( ph -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpanr12  443  mp3an23  1370  equs4  1777  sb4bor  1888  elvd  2826  eueq2dc  2999  sbcgf  3119  csbconstgf  3160  sbcnestg  3201  csbnestg  3202  csbnest1g  3203  ssindif0im  3584  mpteq1  4215  iinexgm  4290  exmid1stab  4345  mss  4366  eusv2nf  4602  eldifpw  4623  ordtriexmid  4668  onsucsssucexmid  4674  ordsucunielexmid  4678  nn0suc  4751  xpss1  4885  xpiindim  4917  reldm0  4999  elrnmpt1s  5032  resdm  5102  resid  5120  eliniseg  5157  trinxp  5181  inimasn  5205  ssrnres  5230  cnveq0  5244  coi2  5304  relrelss  5314  funcnvres  5454  funimaex  5466  fnresin1  5498  fnresin2  5499  fresin  5568  dffv3g  5691  ssimaex  5764  dmfco  5773  fvmpt  5782  fsn  5880  fsn2  5882  funop  5892  elabrex  5963  elabrexg  5964  f1elima  5979  2ndconst  6458  tposfun  6531  tpostpos2  6536  tfrexlem  6605  tfri3  6638  rdgruledefgg  6646  rdgss  6654  frecsuclem  6677  frecrdg  6679  oa0  6730  om0  6731  oei0  6732  oav2  6736  oa1suc  6740  nnmsucr  6761  nnm1  6798  nnm2  6799  ecelqsg  6862  ecidg  6873  xpider  6880  qsel  6886  mapdm0  6937  map0e  6967  mapsnconst  6976  ixpsnf1o  7018  map1  7101  dom1o  7116  xp1en  7121  xpcomco  7124  xpmapenlem  7149  findcard2s  7194  findcard2d  7195  findcard2sd  7196  exmidpw  7215  residfi  7254  fidcenumlemr  7272  sbthlem7  7280  eqinfti  7360  djueq1  7380  omp1eomlem  7434  endjusym  7436  eninl  7437  eninr  7438  difinfsn  7440  finomni  7480  pm54.43  7536  exmidonfinlem  7545  2onetap  7621  mulidpi  7685  nlt1pig  7708  indpi  7709  halfnqq  7777  archnqq  7784  prarloclemarch  7785  prarloclemarch2  7786  nnnq  7789  nq0a0  7824  addpinq1  7831  prarloclemlt  7860  prarloclemlo  7861  prarloclem3  7864  prarloclemcalc  7869  nqprm  7909  addnqpr1  7929  1idprl  7957  1idpru  7958  1idpr  7959  recexprlem1ssl  8000  recexprlem1ssu  8001  ltmprr  8009  0idsr  8134  1idsr  8135  00sr  8136  pn0sr  8138  negexsr  8139  recexgt0sr  8140  ltm1sr  8144  archsr  8149  prsrcl  8151  prsradd  8153  mappsrprg  8171  map2psrprg  8172  elrealeu  8196  pitonnlem1p1  8213  peano2nnnn  8220  ax1rid  8244  axcnre  8248  peano5nnnn  8259  peano2cn  8461  peano2re  8462  addlid  8465  subid  8545  subid1  8546  negid  8573  negeq0  8580  peano2cnm  8592  peano2rem  8593  mul01  8716  lt0neg1  8796  le0neg1  8798  recexre  8906  inelr  8912  rimul  8913  reapmul1  8923  apsqgt0  8929  mulge0  8947  negap0  8958  divvalap  9004  rerecclap  9060  div2negap  9065  divgt0i2i  9247  indconst0  9302  indconst1  9303  peano5nni  9307  nnge1  9327  times2  9433  addltmul  9542  nn0p1nn  9602  peano2nn0  9603  nn0lele2xi  9614  fcdmnn0supp  9615  fcdmnn0fsupp  9616  fcdmnn0suppg  9617  znnnlt1  9692  nn0lt10b  9726  prime  9745  msqznn  9746  zeo  9751  elnn1uz2  10007  qreccl  10042  qdivcl  10043  irrmul  10047  rphalfcl  10082  rpnegap  10087  zgt1rpn0n1  10096  ltpnf  10182  nltmnf  10190  pnfge  10191  xlt0neg1  10240  xle0neg1  10242  xaddpnf1  10248  xaddmnf1  10250  xaddid1  10264  xsubge0  10283  xleaddadd  10289  elioopnf  10369  elicopnf  10371  iccshftri  10397  iccshftli  10399  iccdili  10401  icccntri  10403  fzprval  10489  fzofzp1  10645  fzostep1  10656  flqge0nn0  10728  flqge1nn  10729  fldiv4p1lem1div2  10740  exp1  10982  qexpclz  10997  nn0sqcl  11003  expeq0  11007  expubnd  11033  sqval  11034  sqeq0  11039  resqcl  11044  zsqcl  11047  iexpcyc  11081  binom21  11089  bcnn  11195  bcn2  11202  bcn2p1  11209  bcnm1  11211  fihasheq0  11232  hashsng  11237  fihashen1  11238  fimaxq  11270  hashf1lem2  11286  iswrddm0  11328  ccatval2  11366  ccatsymb  11370  ccatrid  11375  eqs1  11396  s111  11399  swrdnd  11431  pfx00g  11447  shftfibg  11585  shftfib  11588  reim0  11626  imval2  11659  cjap0  11673  cjne0  11674  rexuz3  11756  resqrexlemover  11776  abssq  11847  nn0abscl  11851  nnabscl  11866  abs2dif  11872  max0addsup  11985  climshft  12070  bcxmas  12256  efgt1p2  12462  efgt1p  12463  efi4p  12484  resin4p  12485  recos4p  12486  sinbnd  12519  cosbnd  12520  dvdsval2  12557  zdvdsdc  12579  dvdsmul2  12581  dvdsmulcr  12588  dvdsabseq  12614  divconjdvds  12616  alzdvds  12621  fzo0dvdseq  12624  odd2np1lem  12639  mod2eq1n2dvds  12646  flodddiv4  12703  flodddiv4t2lthalf  12706  bits0  12715  bitsp1o  12720  gcdmndc  12732  gcd0id  12756  gcd1  12764  dfgcd2  12791  gcdmultiple  12797  gcdmultiplez  12798  dvdssq  12808  lcmmndc  12840  lcm0val  12843  dvdslcm  12847  lcmeq0  12849  lcmgcd  12856  lcmdvds  12857  lcmid  12858  lcm1  12859  cncongr2  12882  isprm3  12896  prm2orodd  12904  sqrt2irrap  12958  phiprm  13001  pc0  13083  pcxqcl  13091  pcdvdstr  13106  ballotfilem2  13228  ballotfilemfcc  13233  ballotfilem4  13241  unennn  13288  ennnfonelemim  13315  ctinfom  13319  ctinf  13321  enctlem  13323  elrestr  13601  tgval  13616  tgvalex  13617  xpsfrnel  13665  xpsfeq  13666  xpscf  13668  mulg1  13932  mulgnegnn  13935  ghmghmrn  14066  gsumconstcmn  14166  subrngintm  14520  subrgintm  14551  lsp0  14760  mulgrhm2  14945  zlmlemg  14963  zlmsca  14967  0opn  15107  topopn  15109  0cld  15213  ntropn  15218  ntrtop  15229  ntr0  15235  neipsm  15255  rest0  15280  xmetres  15483  metres  15484  mopnex  15606  tgioo  15655  cnlimcim  15772  cnlimc  15773  dvfre  15811  dveflem  15827  dvef  15828  efcn  15869  sin2pim  15914  cos2pim  15915  sinmpi  15916  cosmpi  15917  sinppi  15918  cosppi  15919  efimpi  15920  sincosq1lem  15926  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  sinq34lt0t  15932  sincosq1eq  15940  abssinper  15947  logrpap0b  15977  loglt1b  15994  rpcxp0  16000  rpcxp1  16001  rpcxpsqrt  16024  logsqrt  16025  rprelogbdiv  16059  lgs0  16132  lgs2  16136  lgsneg  16143  lgsdilem  16146  lgsdir2lem2  16148  lgsdir2lem4  16150  lgsdir2lem5  16151  lgsne0  16157  2lgslem1a2  16206  2lgslem1c  16209  upgr0eop  16363  uspgrushgr  16421  usgruspgr  16424  usgr0eop  16483  0grsubgr  16505  wlklenvclwlk  16614  upgr2wlkdc  16618  clwwlk0on0  16672  konigsbergssiedgwen  16727  bj-inf2vnlem1  16996  pwle2  17028  pwf1oexmid  17029  domomsubct  17031  nninfsellemeqinf  17059  sbthom  17071  qdiff  17098  iswomninnlem  17099  redc0  17107