Theorem reximdv 2591

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)

Hypothesis

Ref	Expression
reximdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		reximdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 2590	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2160  ∃wrex 2469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474

This theorem is referenced by:  r19.12  2596  reusv3  4478  rexxfrd  4481  iunpw  4498  fvelima  5588  carden2bex  7219  prnmaddl  7520  prarloclem5  7530  prarloc2  7534  genprndl  7551  genprndu  7552  ltpopr  7625  recexprlemm  7654  recexprlemopl  7655  recexprlemopu  7657  recexprlem1ssl  7663  recexprlem1ssu  7664  cauappcvgprlemupu  7679  caucvgprlemupu  7702  caucvgprprlemupu  7730  caucvgsrlemoffres  7830  map2psrprg  7835  resqrexlemgt0  11064  subcn2  11354  bezoutlembz  12040  pythagtriplem19  12317  tgcl  14041  neiss  14127  ssnei2  14134  tgcnp  14186  cnptopco  14199  cnptopresti  14215  lmtopcnp  14227  blssexps  14406  blssex  14407  mopni3  14461  neibl  14468  metss  14471  metcnp3  14488  rescncf  14545  limcresi  14612