Description: Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | 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 | 4casesdan | |- ( ph -> th ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 4casesdan.1 | |- ( ( ph /\ ( ps /\ ch ) ) -> th ) |
|
| 2 | 4casesdan.2 | |- ( ( ph /\ ( ps /\ -. ch ) ) -> th ) |
|
| 3 | 4casesdan.3 | |- ( ( ph /\ ( -. ps /\ ch ) ) -> th ) |
|
| 4 | 4casesdan.4 | |- ( ( ph /\ ( -. ps /\ -. ch ) ) -> th ) |
|
| 5 | 1 | expcom | |- ( ( ps /\ ch ) -> ( ph -> th ) ) |
| 6 | 2 | expcom | |- ( ( ps /\ -. ch ) -> ( ph -> th ) ) |
| 7 | 3 | expcom | |- ( ( -. ps /\ ch ) -> ( ph -> th ) ) |
| 8 | 4 | expcom | |- ( ( -. ps /\ -. ch ) -> ( ph -> th ) ) |
| 9 | 5 6 7 8 | 4cases | |- ( ph -> th ) |