Metamath Proof Explorer


Theorem xoror

Description: Exclusive disjunction implies disjunction ("XOR implies OR"). (Contributed by BJ, 19-Apr-2019)

Ref Expression
Assertion xoror ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 xor2 ( ( 𝜑𝜓 ) ↔ ( ( 𝜑𝜓 ) ∧ ¬ ( 𝜑𝜓 ) ) )
2 1 simplbi ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) )