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 ) )