Description: A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | tsna1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tsan1 | ||
2 | notnotb | ||
3 | df-nan | ||
4 | 2 3 | bitr3i | |
5 | 4 | con4bii | |
6 | 5 | orbi2i | |
7 | 1 6 | sylibr |