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  5089  relcoi2  5227  tfrlemi14d  6437  tfri1dALT  6455  mapsncnv  6800  findcard2d  7009  findcard2sd  7010  ac6sfi  7016  xpfi  7050  fifo  7103  updjudhcoinlf  7203  updjudhcoinrg  7204  updjud  7205  casefun  7208  omp1eomlem  7217  difinfsnlem  7222  djufun  7227  ctm  7232  ismkvnex  7278  cauappcvgprlemladd  7801  caucvgprprlemmu  7838  caucvgsrlemfv  7934  recidpirqlemcalc  8000  recidpirq  8001  axaddf  8011  axmulf  8012  xaddpnf1  9998  fldiv4lem1div2  10482  q0mod  10532  q1mod  10533  mulp1mod1  10542  m1modnnsub1  10547  modqm1p1mod0  10552  modqltm1p1mod  10553  bcval5  10940  swrd0g  11146  negfi  11624  xrmaxadd  11657  fprodle  12036  fprodmodd  12037  ege2le3  12067  sinltxirr  12157  p1modz1  12190  moddvds  12195  fsumdvds  12238  oddnn02np1  12276  oddge22np1  12277  evennn02n  12278  evennn2n  12279  bitsinv1lem  12357  3lcm2e6woprm  12493  6lcm4e12  12494  isprm6  12554  sqrt2irraplemnn  12586  fermltl  12641  phisum  12648  odzdvds  12653  reumodprminv  12661  pceu  12703  pcaddlem  12747  pcadd  12748  modxai  12824  modsubi  12827  ennnfonelemp1  12862  ennnfonelemkh  12868  ennnfonelemex  12870  exmidunben  12882  ssomct  12901  ssnnctlemct  12902  strslfv  12962  strleund  13020  prdsval  13190  prdsidlem  13364  pws0g  13368  idmhm  13386  mulgneg2  13577  gsumfzfsumlemm  14434  dvdsrzring  14450  expghmap  14454  zndvds  14496  cnbl0  15091  negfcncf  15163  cnrehmeocntop  15167  divcncfap  15171  dvidlemap  15248  dvidrelem  15249  dvidsslem  15250  dvid  15252  dvidre  15254  dvmulxxbr  15259  dvexp  15268  plycjlemc  15317  plycj  15318  dvply1  15322  dvply2g  15323  sincn  15326  coscn  15327  coseq0q4123  15391  tangtx  15395  cosordlem  15406  wilthlem1  15537  1sgm2ppw  15552  perfectlem2  15557  lgslem1  15562  lgsvalmod  15581  lgsmod  15588  lgsdir2lem5  15594  lgsne0  15600  gausslemma2d  15631  lgseisenlem4  15635  lgseisen  15636  lgsquad2lem1  15643  lgsquad3  15646  2lgslem3a1  15659  2lgslem3b1  15660  2lgslem3c1  15661  2lgslem3d1  15662  pwf1oexmid  16108  nninfsellemdc  16119  trilpolemlt1  16152  apdiff  16159  iswomninnlem  16160