Metamath Proof Explorer

Theorem xoror

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

Ref Expression
Assertion xoror 
|- ( ( ph \/_ ps ) -> ( ph \/ ps ) )

Proof

Step Hyp Ref Expression
1 xor2 
 |-  ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
2 1 simplbi 
 |-  ( ( ph \/_ ps ) -> ( ph \/ ps ) )