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 θ ¬ φ ¬ ψ ¬ φ ψ

Proof

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 θ ¬ φ ¬ ψ ¬ φ ψ