Theorem reximdv 2598

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  r19.12  2603  reusv3  4496  rexxfrd  4499  iunpw  4516  fvelima  5615  carden2bex  7270  prnmaddl  7576  prarloclem5  7586  prarloc2  7590  genprndl  7607  genprndu  7608  ltpopr  7681  recexprlemm  7710  recexprlemopl  7711  recexprlemopu  7713  recexprlem1ssl  7719  recexprlem1ssu  7720  cauappcvgprlemupu  7735  caucvgprlemupu  7758  caucvgprprlemupu  7786  caucvgsrlemoffres  7886  map2psrprg  7891  resqrexlemgt0  11204  subcn2  11495  bezoutlembz  12198  pythagtriplem19  12478  mplsubgfileminv  14334  tgcl  14408  neiss  14494  ssnei2  14501  tgcnp  14553  cnptopco  14566  cnptopresti  14582  lmtopcnp  14594  blssexps  14773  blssex  14774  mopni3  14828  neibl  14835  metss  14838  metcnp3  14855  mpomulcn  14910  rescncf  14925  limcresi  15010  plyss  15082