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  4767  relcoi2  4898  tfrlemi14d  6002  tfri1dALT  6020  findcard2d  6447  findcard2sd  6448  ac6sfi  6454  xpfi  6472  cauappcvgprlemladd  6962  caucvgprprlemmu  6999  caucvgsrlemfv  7081  recidpirqlemcalc  7139  recidpirq  7140  q0mod  9489  q1mod  9490  mulp1mod1  9499  m1modnnsub1  9504  modqm1p1mod0  9509  modqltm1p1mod  9510  ibcval5  9839  negfi  10311  moddvds  10412  oddnn02np1  10487  oddge22np1  10488  evennn02n  10489  evennn2n  10490  3lcm2e6woprm  10675  6lcm4e12  10676  isprm6  10733  sqrt2irraplemnn  10764