Theorem 4cases

Description: Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003)

	Ref	Expression
Hypotheses	4cases.1	|- ( ( ph /\ ps ) -> ch )
	4cases.2	|- ( ( ph /\ -. ps ) -> ch )
	4cases.3	|- ( ( -. ph /\ ps ) -> ch )
	4cases.4	|- ( ( -. ph /\ -. ps ) -> ch )
Assertion	4cases	|- ch

Proof

Step	Hyp	Ref	Expression
1		4cases.1	|- ( ( ph /\ ps ) -> ch )
2		4cases.2	|- ( ( ph /\ -. ps ) -> ch )
3		4cases.3	|- ( ( -. ph /\ ps ) -> ch )
4		4cases.4	|- ( ( -. ph /\ -. ps ) -> ch )
5	1 3	pm2.61ian	|- ( ps -> ch )
6	2 4	pm2.61ian	|- ( -. ps -> ch )
7	5 6	pm2.61i	|- ch