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  4737  relcoi2  4868  tfrlemi14d  5970  findcard2d  6375  findcard2sd  6376  ac6sfi  6379  cauappcvgprlemladd  6848  caucvgprprlemmu  6885  caucvgsrlemfv  6967  recidpirqlemcalc  7025  recidpirq  7026  q0mod  9357  q1mod  9358  mulp1mod1  9367  m1modnnsub1  9372  modqm1p1mod0  9377  modqltm1p1mod  9378  ibcval5  9690  negfi  10110  moddvds  10204  oddnn02np1  10280  oddge22np1  10281  evennn02n  10282  evennn2n  10283  3lcm2e6woprm  10468  6lcm4e12  10469  isprm6  10526  sqrt2irraplemnn  10557