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  5058  relcoi2  5196  tfrlemi14d  6386  tfri1dALT  6404  mapsncnv  6749  findcard2d  6947  findcard2sd  6948  ac6sfi  6954  xpfi  6986  fifo  7039  updjudhcoinlf  7139  updjudhcoinrg  7140  updjud  7141  casefun  7144  omp1eomlem  7153  difinfsnlem  7158  djufun  7163  ctm  7168  ismkvnex  7214  cauappcvgprlemladd  7718  caucvgprprlemmu  7755  caucvgsrlemfv  7851  recidpirqlemcalc  7917  recidpirq  7918  axaddf  7928  axmulf  7929  xaddpnf1  9912  fldiv4lem1div2  10376  q0mod  10426  q1mod  10427  mulp1mod1  10436  m1modnnsub1  10441  modqm1p1mod0  10446  modqltm1p1mod  10447  bcval5  10834  negfi  11371  xrmaxadd  11404  fprodle  11783  fprodmodd  11784  ege2le3  11814  sinltxirr  11904  p1modz1  11937  moddvds  11942  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  3lcm2e6woprm  12224  6lcm4e12  12225  isprm6  12285  sqrt2irraplemnn  12317  fermltl  12372  phisum  12378  odzdvds  12383  reumodprminv  12391  pceu  12433  pcaddlem  12477  pcadd  12478  ennnfonelemp1  12563  ennnfonelemkh  12569  ennnfonelemex  12571  exmidunben  12583  ssomct  12602  ssnnctlemct  12603  strslfv  12663  strleund  12721  idmhm  13041  mulgneg2  13226  gsumfzfsumlemm  14075  dvdsrzring  14091  expghmap  14095  zndvds  14137  cnbl0  14702  negfcncf  14760  cnrehmeocntop  14764  divcncfap  14768  dvidlemap  14845  dvid  14847  dvmulxxbr  14851  dvexp  14860  sincn  14904  coscn  14905  coseq0q4123  14969  tangtx  14973  cosordlem  14984  wilthlem1  15112  lgslem1  15116  lgsvalmod  15135  lgsmod  15142  lgsdir2lem5  15148  lgsne0  15154  gausslemma2d  15185  lgseisenlem4  15189  lgseisen  15190  pwf1oexmid  15490  nninfsellemdc  15500  trilpolemlt1  15531  apdiff  15538  iswomninnlem  15539