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