Theorem reximdv 2533

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

Syntax hints:   → wi 4   ∈ wcel 1480  ∃wrex 2417

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422

This theorem is referenced by:  r19.12  2538  reusv3  4381  rexxfrd  4384  iunpw  4401  fvelima  5473  carden2bex  7045  prnmaddl  7305  prarloclem5  7315  prarloc2  7319  genprndl  7336  genprndu  7337  ltpopr  7410  recexprlemm  7439  recexprlemopl  7440  recexprlemopu  7442  recexprlem1ssl  7448  recexprlem1ssu  7449  cauappcvgprlemupu  7464  caucvgprlemupu  7487  caucvgprprlemupu  7515  caucvgsrlemoffres  7615  map2psrprg  7620  resqrexlemgt0  10799  subcn2  11087  bezoutlembz  11699  tgcl  12243  neiss  12329  ssnei2  12336  tgcnp  12388  cnptopco  12401  cnptopresti  12417  lmtopcnp  12429  blssexps  12608  blssex  12609  mopni3  12663  neibl  12670  metss  12673  metcnp3  12690  rescncf  12747  limcresi  12814