Theorem rexlimdva 2410

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

Ref	Expression
rexlimdva.1	⊢ ((φ ∧ x ∈ A) → (ψ → χ))

Assertion

Ref	Expression
rexlimdva	⊢ (φ → (∃x ∈ A ψ → χ))

Distinct variable groups:   φ,x   χ,x

Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 ⊢ ((φ ∧ x ∈ A) → (ψ → χ))
2	1	ex 108	. 2 ⊢ (φ → (x ∈ A → (ψ → χ)))
3	2	rexlimdv 2409	1 ⊢ (φ → (∃x ∈ A ψ → χ))

Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1375  ∃wrex 2284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1364  ax-ie2 1365  ax-4 1382  ax-17 1401  ax-ial 1410  ax-i5r 1411

This theorem depends on definitions:  df-bi 110  df-nf 1330  df-ral 2288  df-rex 2289

This theorem is referenced by:  rexlimdvaa  2411  rexlimivv  2415  rexlimdvv  2416  ralxfrd  4142  rexxfrd  4143  fvelimab  5152  foco2  5241  elunirn  5328  f1elima  5335  tfrlem5  5847  tfrlemibacc  5856  tfrlemibfn  5858  nnaordex  6006  nnawordex  6007  ectocld  6076  ltexnqq  6253  ltbtwnnqq  6259  prarloclem4  6335  genprndl  6353