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  4931  relcoi2  5069  tfrlemi14d  6230  tfri1dALT  6248  mapsncnv  6589  findcard2d  6785  findcard2sd  6786  ac6sfi  6792  xpfi  6818  fifo  6868  updjudhcoinlf  6965  updjudhcoinrg  6966  updjud  6967  casefun  6970  omp1eomlem  6979  difinfsnlem  6984  djufun  6989  ctm  6994  ismkvnex  7029  cauappcvgprlemladd  7466  caucvgprprlemmu  7503  caucvgsrlemfv  7599  recidpirqlemcalc  7665  recidpirq  7666  axaddf  7676  axmulf  7677  xaddpnf1  9629  q0mod  10128  q1mod  10129  mulp1mod1  10138  m1modnnsub1  10143  modqm1p1mod0  10148  modqltm1p1mod  10149  bcval5  10509  negfi  10999  xrmaxadd  11030  ege2le3  11377  moddvds  11502  oddnn02np1  11577  oddge22np1  11578  evennn02n  11579  evennn2n  11580  3lcm2e6woprm  11767  6lcm4e12  11768  isprm6  11825  sqrt2irraplemnn  11857  ennnfonelemp1  11919  ennnfonelemkh  11925  ennnfonelemex  11927  exmidunben  11939  strslfv  12003  strleund  12047  cnbl0  12703  negfcncf  12758  cnrehmeocntop  12762  dvidlemap  12829  dvid  12831  dvmulxxbr  12835  dvexp  12844  sincn  12858  coscn  12859  coseq0q4123  12915  tangtx  12919  cosordlem  12930  pwf1oexmid  13194  nninfsellemdc  13206  trilpolemlt1  13234