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 ( ∃ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∨ ∃ 𝑥 𝜓 ) )

Proof

Step Hyp Ref Expression
1 19.43 ( ∃ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∨ ∃ 𝑥 𝜓 ) )