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  5129  relcoi2  5267  tfrlemi14d  6499  tfri1dALT  6517  mapsncnv  6864  findcard2d  7080  findcard2sd  7081  ac6sfi  7087  xpfi  7124  fifo  7179  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  casefun  7284  omp1eomlem  7293  difinfsnlem  7298  djufun  7303  ctm  7308  ismkvnex  7354  cauappcvgprlemladd  7878  caucvgprprlemmu  7915  caucvgsrlemfv  8011  recidpirqlemcalc  8077  recidpirq  8078  axaddf  8088  axmulf  8089  xaddpnf1  10081  fldiv4lem1div2  10567  q0mod  10617  q1mod  10618  mulp1mod1  10627  m1modnnsub1  10632  modqm1p1mod0  10637  modqltm1p1mod  10638  bcval5  11025  swrd0g  11241  negfi  11789  xrmaxadd  11822  fprodle  12202  fprodmodd  12203  ege2le3  12233  sinltxirr  12323  p1modz1  12356  moddvds  12361  fsumdvds  12404  oddnn02np1  12442  oddge22np1  12443  evennn02n  12444  evennn2n  12445  bitsinv1lem  12523  3lcm2e6woprm  12659  6lcm4e12  12660  isprm6  12720  sqrt2irraplemnn  12752  fermltl  12807  phisum  12814  odzdvds  12819  reumodprminv  12827  pceu  12869  pcaddlem  12913  pcadd  12914  modxai  12990  modsubi  12993  ennnfonelemp1  13028  ennnfonelemkh  13034  ennnfonelemex  13036  exmidunben  13048  ssomct  13067  ssnnctlemct  13068  strslfv  13128  strleund  13187  prdsval  13357  prdsidlem  13531  pws0g  13535  idmhm  13553  mulgneg2  13744  gsumfzfsumlemm  14603  dvdsrzring  14619  expghmap  14623  zndvds  14665  cnbl0  15260  negfcncf  15332  cnrehmeocntop  15336  divcncfap  15340  dvidlemap  15417  dvidrelem  15418  dvidsslem  15419  dvid  15421  dvidre  15423  dvmulxxbr  15428  dvexp  15437  plycjlemc  15486  plycj  15487  dvply1  15491  dvply2g  15492  sincn  15495  coscn  15496  coseq0q4123  15560  tangtx  15564  cosordlem  15575  wilthlem1  15706  1sgm2ppw  15721  perfectlem2  15726  lgslem1  15731  lgsvalmod  15750  lgsmod  15757  lgsdir2lem5  15763  lgsne0  15769  gausslemma2d  15800  lgseisenlem4  15804  lgseisen  15805  lgsquad2lem1  15812  lgsquad3  15815  2lgslem3a1  15828  2lgslem3b1  15829  2lgslem3c1  15830  2lgslem3d1  15831  uspgr2wlkeq  16218  pwf1oexmid  16603  nninfsellemdc  16615  trilpolemlt1  16648  apdiff  16655  iswomninnlem  16656