Metamath Proof Explorer


Theorem tsxo1

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

Ref Expression
Assertion tsxo1 θ ¬ φ ¬ ψ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 tsbi1 θ ¬ φ ¬ ψ φ ψ
2 xnor φ ψ ¬ φ ψ
3 2 orbi2i ¬ φ ¬ ψ φ ψ ¬ φ ¬ ψ ¬ φ ψ
4 1 3 sylib θ ¬ φ ¬ ψ ¬ φ ψ