Theorem reximdv 2576

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

Syntax hints:   → wi 4   ∈ wcel 2146  ∃wrex 2454

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458  df-rex 2459

This theorem is referenced by:  r19.12  2581  reusv3  4454  rexxfrd  4457  iunpw  4474  fvelima  5559  carden2bex  7178  prnmaddl  7464  prarloclem5  7474  prarloc2  7478  genprndl  7495  genprndu  7496  ltpopr  7569  recexprlemm  7598  recexprlemopl  7599  recexprlemopu  7601  recexprlem1ssl  7607  recexprlem1ssu  7608  cauappcvgprlemupu  7623  caucvgprlemupu  7646  caucvgprprlemupu  7674  caucvgsrlemoffres  7774  map2psrprg  7779  resqrexlemgt0  10995  subcn2  11285  bezoutlembz  11970  pythagtriplem19  12247  tgcl  13115  neiss  13201  ssnei2  13208  tgcnp  13260  cnptopco  13273  cnptopresti  13289  lmtopcnp  13301  blssexps  13480  blssex  13481  mopni3  13535  neibl  13542  metss  13545  metcnp3  13562  rescncf  13619  limcresi  13686