Metamath Proof Explorer


Theorem tsna3

Description: A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018)

Ref Expression
Assertion tsna3 θ ψ φ ψ

Proof

Step Hyp Ref Expression
1 tsan3 θ ψ ¬ φ ψ
2 df-nan φ ψ ¬ φ ψ
3 2 orbi2i ψ φ ψ ψ ¬ φ ψ
4 1 3 sylibr θ ψ φ ψ