Theorem reximdv 2631

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  r19.12  2637  reusv3  4550  rexxfrd  4553  iunpw  4570  fvelima  5684  carden2bex  7358  prnmaddl  7673  prarloclem5  7683  prarloc2  7687  genprndl  7704  genprndu  7705  ltpopr  7778  recexprlemm  7807  recexprlemopl  7808  recexprlemopu  7810  recexprlem1ssl  7816  recexprlem1ssu  7817  cauappcvgprlemupu  7832  caucvgprlemupu  7855  caucvgprprlemupu  7883  caucvgsrlemoffres  7983  map2psrprg  7988  resqrexlemgt0  11526  subcn2  11817  bezoutlembz  12520  pythagtriplem19  12800  mplsubgfileminv  14658  tgcl  14732  neiss  14818  ssnei2  14825  tgcnp  14877  cnptopco  14890  cnptopresti  14906  lmtopcnp  14918  blssexps  15097  blssex  15098  mopni3  15152  neibl  15159  metss  15162  metcnp3  15179  mpomulcn  15234  rescncf  15249  limcresi  15334  plyss  15406  umgrnloop0  15911  uhgr2edg  15998