Metamath Proof Explorer

Theorem exan

Description: Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 13-Jan-2018) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021) (Proof shortened by Wolf Lammen, 6-Nov-2022) Expand hypothesis. (Revised by Steven Nguyen, 19-Jun-2023)

Ref Expression
Hypotheses exan.1 𝑥 𝜑
exan.2 𝜓
Assertion exan 𝑥 ( 𝜑𝜓 )


Step Hyp Ref Expression
1 exan.1 𝑥 𝜑
2 exan.2 𝜓
3 2 jctr ( 𝜑 → ( 𝜑𝜓 ) )
4 1 3 eximii 𝑥 ( 𝜑𝜓 )