Theorem rexlimdva 2427

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

Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1390  ∃wrex 2301

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-i5r 1425

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305  df-rex 2306

This theorem is referenced by:  rexlimdvaa  2428  rexlimivv  2432  rexlimdvv  2433  ralxfrd  4159  rexxfrd  4160  fvelimab  5170  foco2  5259  elunirn  5346  f1elima  5353  tfrlem5  5868  tfrlemibacc  5878  tfrlemibfn  5880  nnaordex  6029  nnawordex  6030  ectocld  6101  ltexnqq  6384  ltbtwnnqq  6391  prarloclem4  6473  prarloc2  6479  genprndl  6497  genprndu  6498  prmuloc2  6538  1idprl  6556  1idpru  6557  recexgt0sr  6653  cnegexlem1  6935  cnegexlem2  6936  renegcl  7020  qmulz  8283  icc0r  8513  frec2uzrand  8818