Description: Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ainaiaandna.1 | ||
Assertion | ainaiaandna |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ainaiaandna.1 | ||
2 | 1 | atnaiana | |
3 | 2 | a1i |