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  5129  relcoi2  5267  tfrlemi14d  6499  tfri1dALT  6517  mapsncnv  6864  findcard2d  7080  findcard2sd  7081  ac6sfi  7087  xpfi  7124  fifo  7179  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  casefun  7284  omp1eomlem  7293  difinfsnlem  7298  djufun  7303  ctm  7308  ismkvnex  7354  cauappcvgprlemladd  7878  caucvgprprlemmu  7915  caucvgsrlemfv  8011  recidpirqlemcalc  8077  recidpirq  8078  axaddf  8088  axmulf  8089  xaddpnf1  10081  fldiv4lem1div2  10568  q0mod  10618  q1mod  10619  mulp1mod1  10628  m1modnnsub1  10633  modqm1p1mod0  10638  modqltm1p1mod  10639  bcval5  11026  swrd0g  11245  negfi  11793  xrmaxadd  11826  fprodle  12206  fprodmodd  12207  ege2le3  12237  sinltxirr  12327  p1modz1  12360  moddvds  12365  fsumdvds  12408  oddnn02np1  12446  oddge22np1  12447  evennn02n  12448  evennn2n  12449  bitsinv1lem  12527  3lcm2e6woprm  12663  6lcm4e12  12664  isprm6  12724  sqrt2irraplemnn  12756  fermltl  12811  phisum  12818  odzdvds  12823  reumodprminv  12831  pceu  12873  pcaddlem  12917  pcadd  12918  modxai  12994  modsubi  12997  ennnfonelemp1  13032  ennnfonelemkh  13038  ennnfonelemex  13040  exmidunben  13052  ssomct  13071  ssnnctlemct  13072  strslfv  13132  strleund  13191  prdsval  13361  prdsidlem  13535  pws0g  13539  idmhm  13557  mulgneg2  13748  gsumfzfsumlemm  14607  dvdsrzring  14623  expghmap  14627  zndvds  14669  cnbl0  15264  negfcncf  15336  cnrehmeocntop  15340  divcncfap  15344  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvid  15425  dvidre  15427  dvmulxxbr  15432  dvexp  15441  plycjlemc  15490  plycj  15491  dvply1  15495  dvply2g  15496  sincn  15499  coscn  15500  coseq0q4123  15564  tangtx  15568  cosordlem  15579  wilthlem1  15710  1sgm2ppw  15725  perfectlem2  15730  lgslem1  15735  lgsvalmod  15754  lgsmod  15761  lgsdir2lem5  15767  lgsne0  15773  gausslemma2d  15804  lgseisenlem4  15808  lgseisen  15809  lgsquad2lem1  15816  lgsquad3  15819  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgslem3d1  15835  uspgr2wlkeq  16222  pwf1oexmid  16626  nninfsellemdc  16638  trilpolemlt1  16671  apdiff  16678  qdiff  16679  iswomninnlem  16680