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  4978  relcoi2  5116  tfrlemi14d  6280  tfri1dALT  6298  mapsncnv  6640  findcard2d  6836  findcard2sd  6837  ac6sfi  6843  xpfi  6874  fifo  6924  updjudhcoinlf  7024  updjudhcoinrg  7025  updjud  7026  casefun  7029  omp1eomlem  7038  difinfsnlem  7043  djufun  7048  ctm  7053  ismkvnex  7098  cauappcvgprlemladd  7578  caucvgprprlemmu  7615  caucvgsrlemfv  7711  recidpirqlemcalc  7777  recidpirq  7778  axaddf  7788  axmulf  7789  xaddpnf1  9750  q0mod  10254  q1mod  10255  mulp1mod1  10264  m1modnnsub1  10269  modqm1p1mod0  10274  modqltm1p1mod  10275  bcval5  10637  negfi  11127  xrmaxadd  11158  fprodle  11537  fprodmodd  11538  ege2le3  11568  p1modz1  11690  moddvds  11695  oddnn02np1  11770  oddge22np1  11771  evennn02n  11772  evennn2n  11773  3lcm2e6woprm  11962  6lcm4e12  11963  isprm6  12021  sqrt2irraplemnn  12053  fermltl  12108  phisum  12114  odzdvds  12119  ennnfonelemp1  12135  ennnfonelemkh  12141  ennnfonelemex  12143  exmidunben  12155  ssomct  12174  ssnnctlemct  12175  strslfv  12234  strleund  12278  cnbl0  12934  negfcncf  12989  cnrehmeocntop  12993  dvidlemap  13060  dvid  13062  dvmulxxbr  13066  dvexp  13075  sincn  13090  coscn  13091  coseq0q4123  13155  tangtx  13159  cosordlem  13170  pwf1oexmid  13571  nninfsellemdc  13582  trilpolemlt1  13612  apdiff  13619  iswomninnlem  13620