Theorem 3pm3.2ni

Description: Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011)

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

Proof

Step	Hyp	Ref	Expression
1		3pm3.2ni.1	|- -. ph
2		3pm3.2ni.2	|- -. ps
3		3pm3.2ni.3	|- -. ch
4	1 2	pm3.2ni	|- -. ( ph \/ ps )
5	4 3	pm3.2ni	|- -. ( ( ph \/ ps ) \/ ch )
6		df-3or	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
7	5 6	mtbir	|- -. ( ph \/ ps \/ ch )