Metamath Proof Explorer
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 |
|
|
|
ecase2d.2 |
|
|
|
ecase2d.3 |
|
|
|
ecase2d.4 |
|
|
Assertion |
ecase2d |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ecase2d.1 |
|
2 |
|
ecase2d.2 |
|
3 |
|
ecase2d.3 |
|
4 |
|
ecase2d.4 |
|
5 |
|
idd |
|
6 |
2
|
pm2.21d |
|
7 |
1 6
|
mpand |
|
8 |
3
|
pm2.21d |
|
9 |
1 8
|
mpand |
|
10 |
7 9
|
jaod |
|
11 |
5 10 4
|
mpjaod |
|