Metamath Proof Explorer


Theorem tsxo3

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

Ref Expression
Assertion tsxo3 ( 𝜃 → ( ( 𝜑 ∨ ¬ 𝜓 ) ∨ ( 𝜑𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 tsbi3 ( 𝜃 → ( ( 𝜑 ∨ ¬ 𝜓 ) ∨ ¬ ( 𝜑𝜓 ) ) )
2 df-xor ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
3 2 bicomi ( ¬ ( 𝜑𝜓 ) ↔ ( 𝜑𝜓 ) )
4 3 orbi2i ( ( ( 𝜑 ∨ ¬ 𝜓 ) ∨ ¬ ( 𝜑𝜓 ) ) ↔ ( ( 𝜑 ∨ ¬ 𝜓 ) ∨ ( 𝜑𝜓 ) ) )
5 1 4 sylib ( 𝜃 → ( ( 𝜑 ∨ ¬ 𝜓 ) ∨ ( 𝜑𝜓 ) ) )