Description: An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | exmid2.1 | |
|
exmid2.2 | |
||
Assertion | exmid2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exmid2.1 | |
|
2 | exmid2.2 | |
|
3 | simpl | |
|
4 | 3 | anim2i | |
5 | 4 | ancoms | |
6 | 5 1 | syl | |
7 | simpr | |
|
8 | 7 | anim2i | |
9 | 8 | ancoms | |
10 | 9 2 | syl | |
11 | 6 10 | pm2.61dan | |