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  5180  relcoi2  5318  supp0  6478  tfrlemi14d  6604  tfri1dALT  6622  mapsncnv  6977  findcard2d  7195  findcard2sd  7196  ac6sfi  7202  xpfi  7239  fifo  7314  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  casefun  7425  omp1eomlem  7434  difinfsnlem  7439  djufun  7444  ctm  7449  ismkvnex  7495  cauappcvgprlemladd  8025  caucvgprprlemmu  8062  caucvgsrlemfv  8158  recidpirqlemcalc  8224  recidpirq  8225  axaddf  8235  axmulf  8236  xaddpnf1  10248  fldiv4lem1div2  10742  q0mod  10792  q1mod  10793  mulp1mod1  10802  m1modnnsub1  10807  modqm1p1mod0  10812  modqltm1p1mod  10813  bcval5  11201  hashmap  11268  swrd0g  11432  negfi  11994  xrmaxadd  12027  fprodle  12407  fprodmodd  12408  ege2le3  12438  sinltxirr  12528  p1modz1  12561  moddvds  12566  fsumdvds  12609  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  bitsinv1lem  12728  3lcm2e6woprm  12864  6lcm4e12  12865  isprm6  12925  sqrt2irraplemnn  12957  fermltl  13012  phisum  13019  odzdvds  13024  reumodprminv  13032  pceu  13074  pcaddlem  13118  pcadd  13119  modxai  13195  modsubi  13198  ballotfilemofi  13219  ballotfilem2  13228  ballotfilemfmpn  13234  ballotfilem1ri  13278  ennnfonelemp1  13297  ennnfonelemkh  13303  ennnfonelemex  13305  exmidunben  13317  ssomct  13336  ssnnctlemct  13337  strslfv  13397  strleund  13457  idmhm  13776  mulgneg2  13959  gsumzfi  14158  prdsval  14173  prdsidlem  14193  pws0g  14213  dvdsrzring  14938  expghmap  14942  zndvds  14984  cnbl0  15635  negfcncf  15707  cnrehmeocntop  15711  divcncfap  15715  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvid  15796  dvidre  15798  dvmulxxbr  15803  dvexp  15812  plycjlemc  15861  plycj  15862  dvply1  15866  dvply2g  15867  sincn  15870  coscn  15871  coseq0q4123  15935  tangtx  15939  cosordlem  15950  log2tlbndlog2  16082  wilthlem1  16094  1sgm2ppw  16109  perfectlem2  16114  lgslem1  16119  lgsvalmod  16138  lgsmod  16145  lgsdir2lem5  16151  lgsne0  16157  gausslemma2d  16188  lgseisenlem4  16192  lgseisen  16193  lgsquad2lem1  16200  lgsquad3  16203  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  uspgr2wlkeq  16606  konigsberglem2  16730  pwf1oexmid  17029  nninfsellemdc  17053  trilpolemlt1  17090  apdiff  17097  qdiff  17098  iswomninnlem  17099