Theorem mp1i 10

Description: Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.)

Hypotheses

Ref	Expression
mp1i.a	|- ph
mp1i.b	|- ( ph -> ps )

Assertion

Ref	Expression
mp1i	|- ( ch -> ps )

Proof of Theorem mp1i

Step	Hyp	Ref	Expression
1		mp1i.a	. . 3 |- ph
2		mp1i.b	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 5	. 2 |- ps
4	3	a1i 9	1 |- ( ch -> ps )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6

This theorem is used by:  poirr2  5183  relcoi2  5321  supp0  6482  tfrlemi14d  6609  tfri1dALT  6627  mapsncnv  6983  findcard2d  7201  findcard2sd  7202  ac6sfi  7208  xpfi  7245  fifo  7319  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  casefun  7431  omp1eomlem  7440  difinfsnlem  7445  djufun  7450  ctm  7455  ismkvnex  7501  cauappcvgprlemladd  8031  caucvgprprlemmu  8068  caucvgsrlemfv  8164  recidpirqlemcalc  8230  recidpirq  8231  axaddf  8241  axmulf  8242  xaddpnf1  10264  fldiv4lem1div2  10762  q0mod  10812  q1mod  10813  mulp1mod1  10822  m1modnnsub1  10827  modqm1p1mod0  10832  modqltm1p1mod  10833  bcval5  11222  hashmap  11289  swrd0g  11453  negfi  12016  xrmaxadd  12051  fprodle  12431  fprodmodd  12432  ege2le3  12462  sinltxirr  12552  p1modz1  12585  moddvds  12590  fsumdvds  12633  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  bitsinv1lem  12752  3lcm2e6woprm  12888  6lcm4e12  12889  isprm6  12950  sqrt2irraplemnn  12983  nn0sqdcq  13012  fermltl  13040  phisum  13047  odzdvds  13052  reumodprminv  13060  pceu  13102  pcaddlem  13146  pcadd  13147  modxai  13223  modsubi  13227  prmlem0  13248  ballotfilemofi  13276  ballotfilem2  13285  ballotfilemfmpn  13291  ballotfilem1ri  13335  ennnfonelemp1  13354  ennnfonelemkh  13360  ennnfonelemex  13362  exmidunben  13374  ssomct  13393  ssnnctlemct  13394  strslfv  13454  strleund  13515  idmhm  13834  mulgneg2  14017  gsumzfi  14247  gsum2dfilem2  14271  prdsval  14279  prdsidlem  14299  pws0g  14319  dvdsrzring  15046  expghmap  15050  zndvds  15092  psrlidmfi  15208  cnbl0  15777  negfcncf  15849  cnrehmeocntop  15853  divcncfap  15857  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvid  15938  dvidre  15940  dvmulxxbr  15945  dvexp  15954  plycjlemc  16003  plycj  16004  dvply1  16008  dvply2g  16009  sincn  16012  coscn  16013  coseq0q4123  16078  tangtx  16082  cosordlem  16094  log2tlbndlog2  16237  wilthlem1  16249  chtqrpcl  16296  1sgm2ppw  16306  perfectlem2  16317  bposlem7  16334  lgslem1  16341  lgsvalmod  16360  lgsmod  16367  lgsdir2lem5  16373  lgsne0  16379  gausslemma2d  16410  lgseisenlem4  16414  lgseisen  16415  lgsquad2lem1  16422  lgsquad3  16425  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  uspgr2wlkeq  16828  konigsberglem2  16952  pwf1oexmid  17251  nninfsellemdc  17276  trilpolemlt1  17314  apdiff  17321  qdiff  17322  iswomninnlem  17323