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