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  10258  fldiv4lem1div2  10755  q0mod  10805  q1mod  10806  mulp1mod1  10815  m1modnnsub1  10820  modqm1p1mod0  10825  modqltm1p1mod  10826  bcval5  11215  hashmap  11282  swrd0g  11446  negfi  12009  xrmaxadd  12043  fprodle  12423  fprodmodd  12424  ege2le3  12454  sinltxirr  12544  p1modz1  12577  moddvds  12582  fsumdvds  12625  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  bitsinv1lem  12744  3lcm2e6woprm  12880  6lcm4e12  12881  isprm6  12942  sqrt2irraplemnn  12975  nn0sqdcq  13004  fermltl  13032  phisum  13039  odzdvds  13044  reumodprminv  13052  pceu  13094  pcaddlem  13138  pcadd  13139  modxai  13215  modsubi  13219  prmlem0  13240  ballotfilemofi  13268  ballotfilem2  13277  ballotfilemfmpn  13283  ballotfilem1ri  13327  ennnfonelemp1  13346  ennnfonelemkh  13352  ennnfonelemex  13354  exmidunben  13366  ssomct  13385  ssnnctlemct  13386  strslfv  13446  strleund  13506  idmhm  13825  mulgneg2  14008  gsumzfi  14207  prdsval  14222  prdsidlem  14242  pws0g  14262  dvdsrzring  14987  expghmap  14991  zndvds  15033  cnbl0  15684  negfcncf  15756  cnrehmeocntop  15760  divcncfap  15764  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvid  15845  dvidre  15847  dvmulxxbr  15852  dvexp  15861  plycjlemc  15910  plycj  15911  dvply1  15915  dvply2g  15916  sincn  15919  coscn  15920  coseq0q4123  15985  tangtx  15989  cosordlem  16000  log2tlbndlog2  16139  wilthlem1  16151  1sgm2ppw  16190  perfectlem2  16198  lgslem1  16217  lgsvalmod  16236  lgsmod  16243  lgsdir2lem5  16249  lgsne0  16255  gausslemma2d  16286  lgseisenlem4  16290  lgseisen  16291  lgsquad2lem1  16298  lgsquad3  16301  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  uspgr2wlkeq  16704  konigsberglem2  16828  pwf1oexmid  17127  nninfsellemdc  17151  trilpolemlt1  17188  apdiff  17195  qdiff  17196  iswomninnlem  17197