Description: Inference from Theorem 19.23 of Margaris p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv . (Contributed by NM, 7-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rexlimdv3a.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝜒 ) | |
Assertion | rexlimdv3a | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdv3a.1 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓 ) → 𝜒 ) | |
2 | 1 | 3exp | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) ) |
3 | 2 | rexlimdv | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) ) |