Theorem mp1i

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

Hypotheses
mp1i.1
\( \vdash \varphi \)
mp1i.2
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \chi \rightarrow \psi \)
Proof
l0
mp1i.1
\( \vdash \varphi \)
mp1i.2
\( \vdash \varphi \rightarrow \psi \)
ax-mp l0 _
a1i _