Theorem rexlimdva 2409

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 2408	1 ⊢ (φ → (∃x ∈ A ψ → χ))

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

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 1315  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  ax-4 1382  ax-17 1401  ax-ial 1410  ax-i5r 1411

This theorem depends on definitions:  df-bi 110  df-nf 1329  df-ral 2287  df-rex 2288

This theorem is referenced by:  rexlimdvaa  2410  rexlimivv  2414  rexlimdvv  2415  ralxfrd  4117  rexxfrd  4118  fvelimab  5121  foco2  5210  elunirn  5297  f1elima  5304  tfrlem5  5817  tfrlemibacc  5826  tfrlemibfn  5828