Metamath Proof Explorer

Theorem exor

Description: Alias for 19.43 for easier lookup. (Contributed by SN, 5-Jul-2025) (New usage is discouraged.)

Ref Expression
Assertion exor 
|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )

Proof

Step Hyp Ref Expression
1 19.43 
 |-  ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )