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  5136  relcoi2  5274  supp0  6416  tfrlemi14d  6542  tfri1dALT  6560  mapsncnv  6907  findcard2d  7123  findcard2sd  7124  ac6sfi  7130  xpfi  7167  fifo  7222  updjudhcoinlf  7322  updjudhcoinrg  7323  updjud  7324  casefun  7327  omp1eomlem  7336  difinfsnlem  7341  djufun  7346  ctm  7351  ismkvnex  7397  cauappcvgprlemladd  7921  caucvgprprlemmu  7958  caucvgsrlemfv  8054  recidpirqlemcalc  8120  recidpirq  8121  axaddf  8131  axmulf  8132  xaddpnf1  10125  fldiv4lem1div2  10613  q0mod  10663  q1mod  10664  mulp1mod1  10673  m1modnnsub1  10678  modqm1p1mod0  10683  modqltm1p1mod  10684  bcval5  11071  swrd0g  11290  negfi  11851  xrmaxadd  11884  fprodle  12264  fprodmodd  12265  ege2le3  12295  sinltxirr  12385  p1modz1  12418  moddvds  12423  fsumdvds  12466  oddnn02np1  12504  oddge22np1  12505  evennn02n  12506  evennn2n  12507  bitsinv1lem  12585  3lcm2e6woprm  12721  6lcm4e12  12722  isprm6  12782  sqrt2irraplemnn  12814  fermltl  12869  phisum  12876  odzdvds  12881  reumodprminv  12889  pceu  12931  pcaddlem  12975  pcadd  12976  modxai  13052  modsubi  13055  ennnfonelemp1  13090  ennnfonelemkh  13096  ennnfonelemex  13098  exmidunben  13110  ssomct  13129  ssnnctlemct  13130  strslfv  13190  strleund  13249  prdsval  13419  prdsidlem  13593  pws0g  13597  idmhm  13615  mulgneg2  13806  gsumfzfsumlemm  14666  dvdsrzring  14682  expghmap  14686  zndvds  14728  cnbl0  15328  negfcncf  15400  cnrehmeocntop  15404  divcncfap  15408  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvid  15489  dvidre  15491  dvmulxxbr  15496  dvexp  15505  plycjlemc  15554  plycj  15555  dvply1  15559  dvply2g  15560  sincn  15563  coscn  15564  coseq0q4123  15628  tangtx  15632  cosordlem  15643  wilthlem1  15777  1sgm2ppw  15792  perfectlem2  15797  lgslem1  15802  lgsvalmod  15821  lgsmod  15828  lgsdir2lem5  15834  lgsne0  15840  gausslemma2d  15871  lgseisenlem4  15875  lgseisen  15876  lgsquad2lem1  15883  lgsquad3  15886  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  uspgr2wlkeq  16289  konigsberglem2  16413  pwf1oexmid  16704  nninfsellemdc  16719  trilpolemlt1  16756  apdiff  16763  qdiff  16764  iswomninnlem  16765