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  4995  relcoi2  5133  tfrlemi14d  6297  tfri1dALT  6315  mapsncnv  6657  findcard2d  6853  findcard2sd  6854  ac6sfi  6860  xpfi  6891  fifo  6941  updjudhcoinlf  7041  updjudhcoinrg  7042  updjud  7043  casefun  7046  omp1eomlem  7055  difinfsnlem  7060  djufun  7065  ctm  7070  ismkvnex  7115  cauappcvgprlemladd  7595  caucvgprprlemmu  7632  caucvgsrlemfv  7728  recidpirqlemcalc  7794  recidpirq  7795  axaddf  7805  axmulf  7806  xaddpnf1  9778  q0mod  10286  q1mod  10287  mulp1mod1  10296  m1modnnsub1  10301  modqm1p1mod0  10306  modqltm1p1mod  10307  bcval5  10672  negfi  11165  xrmaxadd  11198  fprodle  11577  fprodmodd  11578  ege2le3  11608  p1modz1  11730  moddvds  11735  oddnn02np1  11813  oddge22np1  11814  evennn02n  11815  evennn2n  11816  3lcm2e6woprm  12014  6lcm4e12  12015  isprm6  12075  sqrt2irraplemnn  12107  fermltl  12162  phisum  12168  odzdvds  12173  reumodprminv  12181  pceu  12223  pcaddlem  12266  pcadd  12267  ennnfonelemp1  12335  ennnfonelemkh  12341  ennnfonelemex  12343  exmidunben  12355  ssomct  12374  ssnnctlemct  12375  strslfv  12434  strleund  12478  cnbl0  13134  negfcncf  13189  cnrehmeocntop  13193  dvidlemap  13260  dvid  13262  dvmulxxbr  13266  dvexp  13275  sincn  13290  coscn  13291  coseq0q4123  13355  tangtx  13359  cosordlem  13370  lgslem1  13501  lgsvalmod  13520  lgsmod  13527  lgsdir2lem5  13533  lgsne0  13539  pwf1oexmid  13839  nninfsellemdc  13850  trilpolemlt1  13880  apdiff  13887  iswomninnlem  13888