Metamath Proof Explorer


Theorem atnaiana

Description: Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020)

Ref Expression
Hypothesis atnaiana.1
|- ph
Assertion atnaiana
|- -. ( ph -> ( ph /\ -. ph ) )

Proof

Step Hyp Ref Expression
1 atnaiana.1
 |-  ph
2 1 bitru
 |-  ( ph <-> T. )
3 pm3.24
 |-  -. ( ph /\ -. ph )
4 3 bifal
 |-  ( ( ph /\ -. ph ) <-> F. )
5 2 4 aifftbifffaibif
 |-  ( ( ph -> ( ph /\ -. ph ) ) <-> F. )
6 5 aisfina
 |-  -. ( ph -> ( ph /\ -. ph ) )