Description: Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994) (Proof shortened by Wolf Lammen, 22-Dec-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ecase2d.1 | |- ( ph -> ps ) |
|
ecase2d.2 | |- ( ph -> -. ( ps /\ ch ) ) |
||
ecase2d.3 | |- ( ph -> -. ( ps /\ th ) ) |
||
ecase2d.4 | |- ( ph -> ( ta \/ ( ch \/ th ) ) ) |
||
Assertion | ecase2d | |- ( ph -> ta ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ecase2d.1 | |- ( ph -> ps ) |
|
2 | ecase2d.2 | |- ( ph -> -. ( ps /\ ch ) ) |
|
3 | ecase2d.3 | |- ( ph -> -. ( ps /\ th ) ) |
|
4 | ecase2d.4 | |- ( ph -> ( ta \/ ( ch \/ th ) ) ) |
|
5 | idd | |- ( ph -> ( ta -> ta ) ) |
|
6 | 2 | pm2.21d | |- ( ph -> ( ( ps /\ ch ) -> ta ) ) |
7 | 1 6 | mpand | |- ( ph -> ( ch -> ta ) ) |
8 | 3 | pm2.21d | |- ( ph -> ( ( ps /\ th ) -> ta ) ) |
9 | 1 8 | mpand | |- ( ph -> ( th -> ta ) ) |
10 | 7 9 | jaod | |- ( ph -> ( ( ch \/ th ) -> ta ) ) |
11 | 5 10 4 | mpjaod | |- ( ph -> ta ) |