Metamath Proof Explorer


Theorem rexlimddv2

Description: Restricted existential elimination rule of natural deduction. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses rexlimddv2.1 ( 𝜑 → ∃ 𝑥𝐴 𝜓 )
rexlimddv2.2 ( ( ( 𝜑𝑥𝐴 ) ∧ 𝜓 ) → 𝜒 )
Assertion rexlimddv2 ( 𝜑𝜒 )

Proof

Step Hyp Ref Expression
1 rexlimddv2.1 ( 𝜑 → ∃ 𝑥𝐴 𝜓 )
2 rexlimddv2.2 ( ( ( 𝜑𝑥𝐴 ) ∧ 𝜓 ) → 𝜒 )
3 2 anasss ( ( 𝜑 ∧ ( 𝑥𝐴𝜓 ) ) → 𝜒 )
4 1 3 rexlimddv ( 𝜑𝜒 )