Theorem rexlimdva 2738

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 423	. 2 ⊢ (φ → (x ∈ A → (ψ → χ)))
3	2	rexlimdv 2737	1 ⊢ (φ → (∃x ∈ A ψ → χ))

Syntax hints:   → wi 4   ∧ wa 358   ∈ wcel 1710  ∃wrex 2615

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619  df-rex 2620

This theorem is referenced by:  rexlimdvaa  2739  rexlimivv  2743  rexlimdvv  2744  pw1disj  4167  leltfintr  4458  ncfinlower  4483  tfin11  4493  tfinpw1  4494  nnpweq  4523  sfin112  4529  sfindbl  4530  vfinspss  4551  vfinspeqtncv  4553  phi11lem1  4595  foco2  5426  f1elima  5474  ectocld  5991  ncssfin  6151  nntccl  6170  dflec2  6210  leaddc1  6214  leconnnc  6218  tlecg  6229  letc  6230  ce2le  6232  ce0lenc1  6238  nclenn  6248  lemuc1  6252  lecadd2  6265  ncslesuc  6266  nnc3n3p1  6276  nchoicelem17  6303  nchoicelem19  6305  nchoice  6306  dmfrec  6314  fnfreclem3  6317