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 7	. 2 |- ps
4	3	a1i 9	1 |- ( ch -> ps )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-mp 7

This theorem is referenced by:  poirr2  4837  relcoi2  4974  tfrlemi14d  6112  tfri1dALT  6130  mapsncnv  6466  findcard2d  6661  findcard2sd  6662  ac6sfi  6668  xpfi  6694  updjudhcoinlf  6825  updjudhcoinrg  6826  updjud  6827  casefun  6830  djufun  6840  ctm  6845  cauappcvgprlemladd  7278  caucvgprprlemmu  7315  caucvgsrlemfv  7397  recidpirqlemcalc  7455  recidpirq  7456  q0mod  9823  q1mod  9824  mulp1mod1  9833  m1modnnsub1  9838  modqm1p1mod0  9843  modqltm1p1mod  9844  ibcval5  10232  negfi  10720  ege2le3  11022  moddvds  11144  oddnn02np1  11219  oddge22np1  11220  evennn02n  11221  evennn2n  11222  3lcm2e6woprm  11407  6lcm4e12  11408  isprm6  11465  sqrt2irraplemnn  11496  strslfv  11599  strleund  11643  nninfsellemdc  12174