Theorem reximdv 2606

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 2605	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2175  ∃wrex 2484

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488  df-rex 2489

This theorem is referenced by:  r19.12  2611  reusv3  4505  rexxfrd  4508  iunpw  4525  fvelima  5624  carden2bex  7279  prnmaddl  7585  prarloclem5  7595  prarloc2  7599  genprndl  7616  genprndu  7617  ltpopr  7690  recexprlemm  7719  recexprlemopl  7720  recexprlemopu  7722  recexprlem1ssl  7728  recexprlem1ssu  7729  cauappcvgprlemupu  7744  caucvgprlemupu  7767  caucvgprprlemupu  7795  caucvgsrlemoffres  7895  map2psrprg  7900  resqrexlemgt0  11250  subcn2  11541  bezoutlembz  12244  pythagtriplem19  12524  mplsubgfileminv  14380  tgcl  14454  neiss  14540  ssnei2  14547  tgcnp  14599  cnptopco  14612  cnptopresti  14628  lmtopcnp  14640  blssexps  14819  blssex  14820  mopni3  14874  neibl  14881  metss  14884  metcnp3  14901  mpomulcn  14956  rescncf  14971  limcresi  15056  plyss  15128