Theorem imp

Description: Importation inference. (Contributed by NM, 3-Jan-1993) (Proof shortened by Eric Schmidt, 22-Dec-2006)

	Ref	Expression
Hypothesis	imp.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	imp	$$⊢\left(\phi \wedge \psi \right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		imp.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		df-an	$$⊢\left(\phi \wedge \psi \right)\leftrightarrow \neg \left(\phi \to \neg \psi \right)$$
3	1	impi	$$⊢\neg \left(\phi \to \neg \psi \right)\to \chi$$
4	2 3	sylbi	$$⊢\left(\phi \wedge \psi \right)\to \chi$$