Theorem pm3.2ni

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

	Ref	Expression
Hypotheses	pm3.2ni.1	⊢ ¬ 𝜑
	pm3.2ni.2	⊢ ¬ 𝜓
Assertion	pm3.2ni	⊢ ¬ ( 𝜑 ∨ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		pm3.2ni.1	⊢ ¬ 𝜑
2		pm3.2ni.2	⊢ ¬ 𝜓
3		id	⊢ ( 𝜑 → 𝜑 )
4	2	pm2.21i	⊢ ( 𝜓 → 𝜑 )
5	3 4	jaoi	⊢ ( ( 𝜑 ∨ 𝜓 ) → 𝜑 )
6	1 5	mto	⊢ ¬ ( 𝜑 ∨ 𝜓 )