Metamath Proof Explorer
Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997) (Proof shortened by Andrew Salmon, 26-Jun-2011)
|
|
Ref |
Expression |
|
Assertion |
rzal |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ne0i |
|
2 |
1
|
necon2bi |
|
3 |
2
|
pm2.21d |
|
4 |
3
|
ralrimiv |
|