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 )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by:  poirr2  5155  relcoi2  5293  supp0  6438  tfrlemi14d  6564  tfri1dALT  6582  mapsncnv  6930  findcard2d  7148  findcard2sd  7149  ac6sfi  7155  xpfi  7192  fifo  7267  updjudhcoinlf  7371  updjudhcoinrg  7372  updjud  7373  casefun  7376  omp1eomlem  7385  difinfsnlem  7390  djufun  7395  ctm  7400  ismkvnex  7446  cauappcvgprlemladd  7973  caucvgprprlemmu  8010  caucvgsrlemfv  8106  recidpirqlemcalc  8172  recidpirq  8173  axaddf  8183  axmulf  8184  xaddpnf1  10179  fldiv4lem1div2  10667  q0mod  10717  q1mod  10718  mulp1mod1  10727  m1modnnsub1  10732  modqm1p1mod0  10737  modqltm1p1mod  10738  bcval5  11125  hashmap  11192  swrd0g  11352  negfi  11913  xrmaxadd  11946  fprodle  12326  fprodmodd  12327  ege2le3  12357  sinltxirr  12447  p1modz1  12480  moddvds  12485  fsumdvds  12528  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  bitsinv1lem  12647  3lcm2e6woprm  12783  6lcm4e12  12784  isprm6  12844  sqrt2irraplemnn  12876  fermltl  12931  phisum  12938  odzdvds  12943  reumodprminv  12951  pceu  12993  pcaddlem  13037  pcadd  13038  modxai  13114  modsubi  13117  ballotfilemofi  13138  ballotfilem2  13142  ennnfonelemp1  13157  ennnfonelemkh  13163  ennnfonelemex  13165  exmidunben  13177  ssomct  13196  ssnnctlemct  13197  strslfv  13257  strleund  13316  prdsval  13486  prdsidlem  13660  pws0g  13664  idmhm  13682  mulgneg2  13873  gsumfzfsumlemm  14735  dvdsrzring  14751  expghmap  14755  zndvds  14797  cnbl0  15399  negfcncf  15471  cnrehmeocntop  15475  divcncfap  15479  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvid  15560  dvidre  15562  dvmulxxbr  15567  dvexp  15576  plycjlemc  15625  plycj  15626  dvply1  15630  dvply2g  15631  sincn  15634  coscn  15635  coseq0q4123  15699  tangtx  15703  cosordlem  15714  wilthlem1  15848  1sgm2ppw  15863  perfectlem2  15868  lgslem1  15873  lgsvalmod  15892  lgsmod  15899  lgsdir2lem5  15905  lgsne0  15911  gausslemma2d  15942  lgseisenlem4  15946  lgseisen  15947  lgsquad2lem1  15954  lgsquad3  15957  2lgslem3a1  15970  2lgslem3b1  15971  2lgslem3c1  15972  2lgslem3d1  15973  uspgr2wlkeq  16360  konigsberglem2  16484  pwf1oexmid  16773  nninfsellemdc  16788  trilpolemlt1  16825  apdiff  16832  qdiff  16833  iswomninnlem  16834  gfsumz  16869