Metamath Proof Explorer


Theorem tsxo2

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

Ref Expression
Assertion tsxo2 θφψ¬φψ

Proof

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