Theorem reximdv 2492

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

Syntax hints:   → wi 4   ∈ wcel 1448  ∃wrex 2376

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-ral 2380  df-rex 2381

This theorem is referenced by:  r19.12  2497  reusv3  4319  rexxfrd  4322  iunpw  4339  fvelima  5405  carden2bex  6956  prnmaddl  7199  prarloclem5  7209  prarloc2  7213  genprndl  7230  genprndu  7231  ltpopr  7304  recexprlemm  7333  recexprlemopl  7334  recexprlemopu  7336  recexprlem1ssl  7342  recexprlem1ssu  7343  cauappcvgprlemupu  7358  caucvgprlemupu  7381  caucvgprprlemupu  7409  caucvgsrlemoffres  7495  resqrexlemgt0  10632  subcn2  10919  bezoutlembz  11485  tgcl  12015  neiss  12101  ssnei2  12108  tgcnp  12159  cnptopco  12172  cnptopresti  12188  lmtopcnp  12200  blssexps  12357  blssex  12358  mopni3  12412  neibl  12419  metss  12422  metcnp3  12435  rescncf  12481  limcresi  12515