Theorem pm3.2ni

Description: Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995)

	Ref	Expression
Hypotheses	pm3.2ni.1	$$⊢\neg \phi$$
	pm3.2ni.2	$$⊢\neg \psi$$
Assertion	pm3.2ni	$$⊢\neg \left(\phi \vee \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		pm3.2ni.1	$$⊢\neg \phi$$
2		pm3.2ni.2	$$⊢\neg \psi$$
3		id	$$⊢\phi \to \phi$$
4	2	pm2.21i	$$⊢\psi \to \phi$$
5	3 4	jaoi	$$⊢\left(\phi \vee \psi \right)\to \phi$$
6	1 5	mto	$$⊢\neg \left(\phi \vee \psi \right)$$