Theorem reximdv 2567

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

Syntax hints:   → wi 4   ∈ wcel 2136  ∃wrex 2445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449  df-rex 2450

This theorem is referenced by:  r19.12  2572  reusv3  4438  rexxfrd  4441  iunpw  4458  fvelima  5538  carden2bex  7145  prnmaddl  7431  prarloclem5  7441  prarloc2  7445  genprndl  7462  genprndu  7463  ltpopr  7536  recexprlemm  7565  recexprlemopl  7566  recexprlemopu  7568  recexprlem1ssl  7574  recexprlem1ssu  7575  cauappcvgprlemupu  7590  caucvgprlemupu  7613  caucvgprprlemupu  7641  caucvgsrlemoffres  7741  map2psrprg  7746  resqrexlemgt0  10962  subcn2  11252  bezoutlembz  11937  pythagtriplem19  12214  tgcl  12714  neiss  12800  ssnei2  12807  tgcnp  12859  cnptopco  12872  cnptopresti  12888  lmtopcnp  12900  blssexps  13079  blssex  13080  mopni3  13134  neibl  13141  metss  13144  metcnp3  13161  rescncf  13218  limcresi  13285