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  7421  updjudhcoinrg  7422  updjud  7423  casefun  7426  omp1eomlem  7435  difinfsnlem  7440  djufun  7445  ctm  7450  ismkvnex  7496  cauappcvgprlemladd  8026  caucvgprprlemmu  8063  caucvgsrlemfv  8159  recidpirqlemcalc  8225  recidpirq  8226  axaddf  8236  axmulf  8237  xaddpnf1  10259  fldiv4lem1div2  10757  q0mod  10807  q1mod  10808  mulp1mod1  10817  m1modnnsub1  10822  modqm1p1mod0  10827  modqltm1p1mod  10828  bcval5  11217  hashmap  11284  swrd0g  11448  negfi  12011  xrmaxadd  12046  fprodle  12426  fprodmodd  12427  ege2le3  12457  sinltxirr  12547  p1modz1  12580  moddvds  12585  fsumdvds  12628  oddnn02np1  12666  oddge22np1  12667  evennn02n  12668  evennn2n  12669  bitsinv1lem  12747  3lcm2e6woprm  12883  6lcm4e12  12884  isprm6  12945  sqrt2irraplemnn  12978  nn0sqdcq  13007  fermltl  13035  phisum  13042  odzdvds  13047  reumodprminv  13055  pceu  13097  pcaddlem  13141  pcadd  13142  modxai  13218  modsubi  13222  prmlem0  13243  ballotfilemofi  13271  ballotfilem2  13280  ballotfilemfmpn  13286  ballotfilem1ri  13330  ennnfonelemp1  13349  ennnfonelemkh  13355  ennnfonelemex  13357  exmidunben  13369  ssomct  13388  ssnnctlemct  13389  strslfv  13449  strleund  13510  idmhm  13829  mulgneg2  14012  gsumzfi  14242  prdsval  14257  prdsidlem  14277  pws0g  14297  dvdsrzring  15022  expghmap  15026  zndvds  15068  cnbl0  15726  negfcncf  15798  cnrehmeocntop  15802  divcncfap  15806  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvid  15887  dvidre  15889  dvmulxxbr  15894  dvexp  15903  plycjlemc  15952  plycj  15953  dvply1  15957  dvply2g  15958  sincn  15961  coscn  15962  coseq0q4123  16027  tangtx  16031  cosordlem  16042  log2tlbndlog2  16181  wilthlem1  16193  chtqrpcl  16240  1sgm2ppw  16250  perfectlem2  16261  bposlem7  16278  lgslem1  16285  lgsvalmod  16304  lgsmod  16311  lgsdir2lem5  16317  lgsne0  16323  gausslemma2d  16354  lgseisenlem4  16358  lgseisen  16359  lgsquad2lem1  16366  lgsquad3  16369  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  uspgr2wlkeq  16772  konigsberglem2  16896  pwf1oexmid  17195  nninfsellemdc  17219  trilpolemlt1  17257  apdiff  17264  qdiff  17265  iswomninnlem  17266