Metamath Proof Explorer


Theorem ainaiaandna

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 φ ¬ φ φ ¬ φ

Proof

Step Hyp Ref Expression
1 ainaiaandna.1 φ
2 1 atnaiana ¬ φ φ ¬ φ
3 2 a1i φ ¬ φ φ ¬ φ