Theorem mp1i 10

Description: Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.)

Hypotheses

Ref	Expression
mp1i.a	⊢ 𝜑
mp1i.b	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
mp1i	⊢ (𝜒 → 𝜓)

Proof of Theorem mp1i

Step	Hyp	Ref	Expression
1		mp1i.a	. . 3 ⊢ 𝜑
2		mp1i.b	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 7	. 2 ⊢ 𝜓
4	3	a1i 9	1 ⊢ (𝜒 → 𝜓)

Syntax hints:   → wi 4

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

This theorem is referenced by:  poirr2  4742  relcoi2  4873  tfrlemi14d  5975  findcard2d  6376  findcard2sd  6377  ac6sfi  6380  cauappcvgprlemladd  6784  caucvgprprlemmu  6821  caucvgsrlemfv  6903  recidpirqlemcalc  6961  recidpirq  6962  q0mod  9270  q1mod  9271  mulp1mod1  9280  m1modnnsub1  9285  modqm1p1mod0  9290  modqltm1p1mod  9291  ibcval5  9595  moddvds  10080  oddnn02np1  10155  oddge22np1  10156  evennn02n  10157  evennn2n  10158