Metamath Proof Explorer
Description: Deduction for elimination by cases. (Contributed by NM, 24-May-2013)
|
|
Ref |
Expression |
|
Hypotheses |
ecase3ad.1 |
|
|
|
ecase3ad.2 |
|
|
|
ecase3ad.3 |
|
|
Assertion |
ecase3ad |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ecase3ad.1 |
|
2 |
|
ecase3ad.2 |
|
3 |
|
ecase3ad.3 |
|
4 |
|
notnotr |
|
5 |
4 1
|
syl5 |
|
6 |
|
notnotr |
|
7 |
6 2
|
syl5 |
|
8 |
5 7 3
|
ecased |
|