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 ( 𝜃 → ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ∨ ¬ ( 𝜑𝜓 ) ) )