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  5063  relcoi2  5201  tfrlemi14d  6400  tfri1dALT  6418  mapsncnv  6763  findcard2d  6961  findcard2sd  6962  ac6sfi  6968  xpfi  7002  fifo  7055  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  casefun  7160  omp1eomlem  7169  difinfsnlem  7174  djufun  7179  ctm  7184  ismkvnex  7230  cauappcvgprlemladd  7742  caucvgprprlemmu  7779  caucvgsrlemfv  7875  recidpirqlemcalc  7941  recidpirq  7942  axaddf  7952  axmulf  7953  xaddpnf1  9938  fldiv4lem1div2  10414  q0mod  10464  q1mod  10465  mulp1mod1  10474  m1modnnsub1  10479  modqm1p1mod0  10484  modqltm1p1mod  10485  bcval5  10872  negfi  11410  xrmaxadd  11443  fprodle  11822  fprodmodd  11823  ege2le3  11853  sinltxirr  11943  p1modz1  11976  moddvds  11981  fsumdvds  12024  oddnn02np1  12062  oddge22np1  12063  evennn02n  12064  evennn2n  12065  bitsinv1lem  12143  3lcm2e6woprm  12279  6lcm4e12  12280  isprm6  12340  sqrt2irraplemnn  12372  fermltl  12427  phisum  12434  odzdvds  12439  reumodprminv  12447  pceu  12489  pcaddlem  12533  pcadd  12534  modxai  12610  modsubi  12613  ennnfonelemp1  12648  ennnfonelemkh  12654  ennnfonelemex  12656  exmidunben  12668  ssomct  12687  ssnnctlemct  12688  strslfv  12748  strleund  12806  prdsval  12975  prdsidlem  13149  pws0g  13153  idmhm  13171  mulgneg2  13362  gsumfzfsumlemm  14219  dvdsrzring  14235  expghmap  14239  zndvds  14281  cnbl0  14854  negfcncf  14926  cnrehmeocntop  14930  divcncfap  14934  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvid  15015  dvidre  15017  dvmulxxbr  15022  dvexp  15031  plycjlemc  15080  plycj  15081  dvply1  15085  dvply2g  15086  sincn  15089  coscn  15090  coseq0q4123  15154  tangtx  15158  cosordlem  15169  wilthlem1  15300  1sgm2ppw  15315  perfectlem2  15320  lgslem1  15325  lgsvalmod  15344  lgsmod  15351  lgsdir2lem5  15357  lgsne0  15363  gausslemma2d  15394  lgseisenlem4  15398  lgseisen  15399  lgsquad2lem1  15406  lgsquad3  15409  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  pwf1oexmid  15730  nninfsellemdc  15741  trilpolemlt1  15772  apdiff  15779  iswomninnlem  15780