This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexlimd3

Description: * Inference from Theorem 19.23 of Margaris p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses rexlimd3.1 ⊢ Ⅎ 𝑥 𝜑
rexlimd3.2 ⊢ Ⅎ 𝑥 𝜒
rexlimd3.3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
Assertion rexlimd3 ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )

Proof

Step Hyp Ref Expression
1 rexlimd3.1 ⊢ Ⅎ 𝑥 𝜑
2 rexlimd3.2 ⊢ Ⅎ 𝑥 𝜒
3 rexlimd3.3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
4 3 exp31 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
5 1 2 4 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )