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  6498  tfri1dALT  6516  mapsncnv  6863  findcard2d  7079  findcard2sd  7080  ac6sfi  7086  xpfi  7123  fifo  7178  updjudhcoinlf  7278  updjudhcoinrg  7279  updjud  7280  casefun  7283  omp1eomlem  7292  difinfsnlem  7297  djufun  7302  ctm  7307  ismkvnex  7353  cauappcvgprlemladd  7877  caucvgprprlemmu  7914  caucvgsrlemfv  8010  recidpirqlemcalc  8076  recidpirq  8077  axaddf  8087  axmulf  8088  xaddpnf1  10080  fldiv4lem1div2  10566  q0mod  10616  q1mod  10617  mulp1mod1  10626  m1modnnsub1  10631  modqm1p1mod0  10636  modqltm1p1mod  10637  bcval5  11024  swrd0g  11240  negfi  11788  xrmaxadd  11821  fprodle  12200  fprodmodd  12201  ege2le3  12231  sinltxirr  12321  p1modz1  12354  moddvds  12359  fsumdvds  12402  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  bitsinv1lem  12521  3lcm2e6woprm  12657  6lcm4e12  12658  isprm6  12718  sqrt2irraplemnn  12750  fermltl  12805  phisum  12812  odzdvds  12817  reumodprminv  12825  pceu  12867  pcaddlem  12911  pcadd  12912  modxai  12988  modsubi  12991  ennnfonelemp1  13026  ennnfonelemkh  13032  ennnfonelemex  13034  exmidunben  13046  ssomct  13065  ssnnctlemct  13066  strslfv  13126  strleund  13185  prdsval  13355  prdsidlem  13529  pws0g  13533  idmhm  13551  mulgneg2  13742  gsumfzfsumlemm  14600  dvdsrzring  14616  expghmap  14620  zndvds  14662  cnbl0  15257  negfcncf  15329  cnrehmeocntop  15333  divcncfap  15337  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvid  15418  dvidre  15420  dvmulxxbr  15425  dvexp  15434  plycjlemc  15483  plycj  15484  dvply1  15488  dvply2g  15489  sincn  15492  coscn  15493  coseq0q4123  15557  tangtx  15561  cosordlem  15572  wilthlem1  15703  1sgm2ppw  15718  perfectlem2  15723  lgslem1  15728  lgsvalmod  15747  lgsmod  15754  lgsdir2lem5  15760  lgsne0  15766  gausslemma2d  15797  lgseisenlem4  15801  lgseisen  15802  lgsquad2lem1  15809  lgsquad3  15812  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  uspgr2wlkeq  16215  pwf1oexmid  16600  nninfsellemdc  16612  trilpolemlt1  16645  apdiff  16652  iswomninnlem  16653