Theorem reximdv 2651

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  r19.12  2657  reusv3  4606  rexxfrd  4609  iunpw  4626  fvelima  5754  carden2bex  7536  prnmaddl  7858  prarloclem5  7868  prarloc2  7872  genprndl  7889  genprndu  7890  ltpopr  7963  recexprlemm  7992  recexprlemopl  7993  recexprlemopu  7995  recexprlem1ssl  8001  recexprlem1ssu  8002  cauappcvgprlemupu  8017  caucvgprlemupu  8040  caucvgprprlemupu  8068  caucvgsrlemoffres  8168  map2psrprg  8173  resqrexlemgt0  11802  subcn2  12096  bezoutlembz  12800  pythagtriplem19  13084  mplsubgfileminv  15182  tgcl  15256  neiss  15342  ssnei2  15349  tgcnp  15401  cnptopco  15414  cnptopresti  15430  lmtopcnp  15442  blssexps  15621  blssex  15622  mopni3  15676  neibl  15683  metss  15686  metcnp3  15703  mpomulcn  15758  rescncf  15773  limcresi  15858  plyss  15930  umgrnloop0  16524  uhgr2edg  16613