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  5127  relcoi2  5265  tfrlemi14d  6494  tfri1dALT  6512  mapsncnv  6859  findcard2d  7073  findcard2sd  7074  ac6sfi  7080  xpfi  7117  fifo  7170  updjudhcoinlf  7270  updjudhcoinrg  7271  updjud  7272  casefun  7275  omp1eomlem  7284  difinfsnlem  7289  djufun  7294  ctm  7299  ismkvnex  7345  cauappcvgprlemladd  7868  caucvgprprlemmu  7905  caucvgsrlemfv  8001  recidpirqlemcalc  8067  recidpirq  8068  axaddf  8078  axmulf  8079  xaddpnf1  10071  fldiv4lem1div2  10557  q0mod  10607  q1mod  10608  mulp1mod1  10617  m1modnnsub1  10622  modqm1p1mod0  10627  modqltm1p1mod  10628  bcval5  11015  swrd0g  11231  negfi  11779  xrmaxadd  11812  fprodle  12191  fprodmodd  12192  ege2le3  12222  sinltxirr  12312  p1modz1  12345  moddvds  12350  fsumdvds  12393  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  bitsinv1lem  12512  3lcm2e6woprm  12648  6lcm4e12  12649  isprm6  12709  sqrt2irraplemnn  12741  fermltl  12796  phisum  12803  odzdvds  12808  reumodprminv  12816  pceu  12858  pcaddlem  12902  pcadd  12903  modxai  12979  modsubi  12982  ennnfonelemp1  13017  ennnfonelemkh  13023  ennnfonelemex  13025  exmidunben  13037  ssomct  13056  ssnnctlemct  13057  strslfv  13117  strleund  13176  prdsval  13346  prdsidlem  13520  pws0g  13524  idmhm  13542  mulgneg2  13733  gsumfzfsumlemm  14591  dvdsrzring  14607  expghmap  14611  zndvds  14653  cnbl0  15248  negfcncf  15320  cnrehmeocntop  15324  divcncfap  15328  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvid  15409  dvidre  15411  dvmulxxbr  15416  dvexp  15425  plycjlemc  15474  plycj  15475  dvply1  15479  dvply2g  15480  sincn  15483  coscn  15484  coseq0q4123  15548  tangtx  15552  cosordlem  15563  wilthlem1  15694  1sgm2ppw  15709  perfectlem2  15714  lgslem1  15719  lgsvalmod  15738  lgsmod  15745  lgsdir2lem5  15751  lgsne0  15757  gausslemma2d  15788  lgseisenlem4  15792  lgseisen  15793  lgsquad2lem1  15800  lgsquad3  15803  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  uspgr2wlkeq  16162  pwf1oexmid  16536  nninfsellemdc  16548  trilpolemlt1  16581  apdiff  16588  iswomninnlem  16589