Theorem 4casesdan 991

Description: Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)

Hypotheses

Ref	Expression
4casesdan.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )
4casesdan.2	|- ( ( ph /\ ( ps /\ -. ch ) ) -> th )
4casesdan.3	|- ( ( ph /\ ( -. ps /\ ch ) ) -> th )
4casesdan.4	|- ( ( ph /\ ( -. ps /\ -. ch ) ) -> th )

Assertion

Ref	Expression
4casesdan	|- ( ph -> th )

Proof of Theorem 4casesdan

Step	Hyp	Ref	Expression
1		4casesdan.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	expcom 451	. 2 |- ( ( ps /\ ch ) -> ( ph -> th ) )
3		4casesdan.2	. . 3 |- ( ( ph /\ ( ps /\ -. ch ) ) -> th )
4	3	expcom 451	. 2 |- ( ( ps /\ -. ch ) -> ( ph -> th ) )
5		4casesdan.3	. . 3 |- ( ( ph /\ ( -. ps /\ ch ) ) -> th )
6	5	expcom 451	. 2 |- ( ( -. ps /\ ch ) -> ( ph -> th ) )
7		4casesdan.4	. . 3 |- ( ( ph /\ ( -. ps /\ -. ch ) ) -> th )
8	7	expcom 451	. 2 |- ( ( -. ps /\ -. ch ) -> ( ph -> th ) )
9	2, 4, 6, 8	4cases 990	1 |- ( ph -> th )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  unxpdomlem3  8166  mndifsplit  20442  cdleme41snaw  35764  dihord  36553  dihjat  36712