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  5074  relcoi2  5212  tfrlemi14d  6418  tfri1dALT  6436  mapsncnv  6781  findcard2d  6987  findcard2sd  6988  ac6sfi  6994  xpfi  7028  fifo  7081  updjudhcoinlf  7181  updjudhcoinrg  7182  updjud  7183  casefun  7186  omp1eomlem  7195  difinfsnlem  7200  djufun  7205  ctm  7210  ismkvnex  7256  cauappcvgprlemladd  7770  caucvgprprlemmu  7807  caucvgsrlemfv  7903  recidpirqlemcalc  7969  recidpirq  7970  axaddf  7980  axmulf  7981  xaddpnf1  9967  fldiv4lem1div2  10448  q0mod  10498  q1mod  10499  mulp1mod1  10508  m1modnnsub1  10513  modqm1p1mod0  10518  modqltm1p1mod  10519  bcval5  10906  negfi  11510  xrmaxadd  11543  fprodle  11922  fprodmodd  11923  ege2le3  11953  sinltxirr  12043  p1modz1  12076  moddvds  12081  fsumdvds  12124  oddnn02np1  12162  oddge22np1  12163  evennn02n  12164  evennn2n  12165  bitsinv1lem  12243  3lcm2e6woprm  12379  6lcm4e12  12380  isprm6  12440  sqrt2irraplemnn  12472  fermltl  12527  phisum  12534  odzdvds  12539  reumodprminv  12547  pceu  12589  pcaddlem  12633  pcadd  12634  modxai  12710  modsubi  12713  ennnfonelemp1  12748  ennnfonelemkh  12754  ennnfonelemex  12756  exmidunben  12768  ssomct  12787  ssnnctlemct  12788  strslfv  12848  strleund  12906  prdsval  13076  prdsidlem  13250  pws0g  13254  idmhm  13272  mulgneg2  13463  gsumfzfsumlemm  14320  dvdsrzring  14336  expghmap  14340  zndvds  14382  cnbl0  14977  negfcncf  15049  cnrehmeocntop  15053  divcncfap  15057  dvidlemap  15134  dvidrelem  15135  dvidsslem  15136  dvid  15138  dvidre  15140  dvmulxxbr  15145  dvexp  15154  plycjlemc  15203  plycj  15204  dvply1  15208  dvply2g  15209  sincn  15212  coscn  15213  coseq0q4123  15277  tangtx  15281  cosordlem  15292  wilthlem1  15423  1sgm2ppw  15438  perfectlem2  15443  lgslem1  15448  lgsvalmod  15467  lgsmod  15474  lgsdir2lem5  15480  lgsne0  15486  gausslemma2d  15517  lgseisenlem4  15521  lgseisen  15522  lgsquad2lem1  15529  lgsquad3  15532  2lgslem3a1  15545  2lgslem3b1  15546  2lgslem3c1  15547  2lgslem3d1  15548  pwf1oexmid  15898  nninfsellemdc  15909  trilpolemlt1  15942  apdiff  15949  iswomninnlem  15950