Theorem pm3.2ni

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

	Ref	Expression
Hypotheses	pm3.2ni.1	|- -. ph
	pm3.2ni.2	|- -. ps
Assertion	pm3.2ni	|- -. ( ph \/ ps )

Proof

Step	Hyp	Ref	Expression
1		pm3.2ni.1	|- -. ph
2		pm3.2ni.2	|- -. ps
3		id	|- ( ph -> ph )
4	2	pm2.21i	|- ( ps -> ph )
5	3 4	jaoi	|- ( ( ph \/ ps ) -> ph )
6	1 5	mto	|- -. ( ph \/ ps )