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  5160  relcoi2  5298  supp0  6451  tfrlemi14d  6577  tfri1dALT  6595  mapsncnv  6943  findcard2d  7161  findcard2sd  7162  ac6sfi  7168  xpfi  7205  fifo  7280  updjudhcoinlf  7384  updjudhcoinrg  7385  updjud  7386  casefun  7389  omp1eomlem  7398  difinfsnlem  7403  djufun  7408  ctm  7413  ismkvnex  7459  cauappcvgprlemladd  7989  caucvgprprlemmu  8026  caucvgsrlemfv  8122  recidpirqlemcalc  8188  recidpirq  8189  axaddf  8199  axmulf  8200  xaddpnf1  10198  fldiv4lem1div2  10691  q0mod  10741  q1mod  10742  mulp1mod1  10751  m1modnnsub1  10756  modqm1p1mod0  10761  modqltm1p1mod  10762  bcval5  11150  hashmap  11217  swrd0g  11377  negfi  11938  xrmaxadd  11971  fprodle  12351  fprodmodd  12352  ege2le3  12382  sinltxirr  12472  p1modz1  12505  moddvds  12510  fsumdvds  12553  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  bitsinv1lem  12672  3lcm2e6woprm  12808  6lcm4e12  12809  isprm6  12869  sqrt2irraplemnn  12901  fermltl  12956  phisum  12963  odzdvds  12968  reumodprminv  12976  pceu  13018  pcaddlem  13062  pcadd  13063  modxai  13139  modsubi  13142  ballotfilemofi  13163  ballotfilem2  13172  ballotfilemfmpn  13178  ballotfilem1ri  13222  ennnfonelemp1  13241  ennnfonelemkh  13247  ennnfonelemex  13249  exmidunben  13261  ssomct  13280  ssnnctlemct  13281  strslfv  13341  strleund  13400  idmhm  13724  mulgneg2  13909  gfsumz  14109  prdsval  14115  prdsidlem  14135  pws0g  14155  gsumfzfsumlemm  14861  dvdsrzring  14877  expghmap  14881  zndvds  14923  cnbl0  15525  negfcncf  15597  cnrehmeocntop  15601  divcncfap  15605  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvid  15686  dvidre  15688  dvmulxxbr  15693  dvexp  15702  plycjlemc  15751  plycj  15752  dvply1  15756  dvply2g  15757  sincn  15760  coscn  15761  coseq0q4123  15825  tangtx  15829  cosordlem  15840  wilthlem1  15974  1sgm2ppw  15989  perfectlem2  15994  lgslem1  15999  lgsvalmod  16018  lgsmod  16025  lgsdir2lem5  16031  lgsne0  16037  gausslemma2d  16068  lgseisenlem4  16072  lgseisen  16073  lgsquad2lem1  16080  lgsquad3  16083  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  uspgr2wlkeq  16486  konigsberglem2  16610  pwf1oexmid  16899  nninfsellemdc  16914  trilpolemlt1  16951  apdiff  16958  qdiff  16959  iswomninnlem  16960