Metamath Proof Explorer


Theorem tsna1

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

Proof

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