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  5075  relcoi2  5213  tfrlemi14d  6419  tfri1dALT  6437  mapsncnv  6782  findcard2d  6988  findcard2sd  6989  ac6sfi  6995  xpfi  7029  fifo  7082  updjudhcoinlf  7182  updjudhcoinrg  7183  updjud  7184  casefun  7187  omp1eomlem  7196  difinfsnlem  7201  djufun  7206  ctm  7211  ismkvnex  7257  cauappcvgprlemladd  7771  caucvgprprlemmu  7808  caucvgsrlemfv  7904  recidpirqlemcalc  7970  recidpirq  7971  axaddf  7981  axmulf  7982  xaddpnf1  9968  fldiv4lem1div2  10450  q0mod  10500  q1mod  10501  mulp1mod1  10510  m1modnnsub1  10515  modqm1p1mod0  10520  modqltm1p1mod  10521  bcval5  10908  swrd0g  11113  negfi  11539  xrmaxadd  11572  fprodle  11951  fprodmodd  11952  ege2le3  11982  sinltxirr  12072  p1modz1  12105  moddvds  12110  fsumdvds  12153  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  bitsinv1lem  12272  3lcm2e6woprm  12408  6lcm4e12  12409  isprm6  12469  sqrt2irraplemnn  12501  fermltl  12556  phisum  12563  odzdvds  12568  reumodprminv  12576  pceu  12618  pcaddlem  12662  pcadd  12663  modxai  12739  modsubi  12742  ennnfonelemp1  12777  ennnfonelemkh  12783  ennnfonelemex  12785  exmidunben  12797  ssomct  12816  ssnnctlemct  12817  strslfv  12877  strleund  12935  prdsval  13105  prdsidlem  13279  pws0g  13283  idmhm  13301  mulgneg2  13492  gsumfzfsumlemm  14349  dvdsrzring  14365  expghmap  14369  zndvds  14411  cnbl0  15006  negfcncf  15078  cnrehmeocntop  15082  divcncfap  15086  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvid  15167  dvidre  15169  dvmulxxbr  15174  dvexp  15183  plycjlemc  15232  plycj  15233  dvply1  15237  dvply2g  15238  sincn  15241  coscn  15242  coseq0q4123  15306  tangtx  15310  cosordlem  15321  wilthlem1  15452  1sgm2ppw  15467  perfectlem2  15472  lgslem1  15477  lgsvalmod  15496  lgsmod  15503  lgsdir2lem5  15509  lgsne0  15515  gausslemma2d  15546  lgseisenlem4  15550  lgseisen  15551  lgsquad2lem1  15558  lgsquad3  15561  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  pwf1oexmid  15936  nninfsellemdc  15947  trilpolemlt1  15980  apdiff  15987  iswomninnlem  15988