Theorem mp1i

Description: Inference detaching an antecedent and introducing a new one. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypotheses	mp1i.1	$$⊢\phi$$
	mp1i.2	$$⊢\phi \to \psi$$
Assertion	mp1i	$$⊢\chi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		mp1i.1	$$⊢\phi$$
2		mp1i.2	$$⊢\phi \to \psi$$
3	1 2	ax-mp	$$⊢\psi$$
4	3	a1i	$$⊢\chi \to \psi$$