Theorem reximdv 2643

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

Syntax hints:   → wi 4   ∈ wcel 2203  ∃wrex 2521

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  r19.12  2649  reusv3  4581  rexxfrd  4584  iunpw  4601  fvelima  5728  carden2bex  7486  prnmaddl  7805  prarloclem5  7815  prarloc2  7819  genprndl  7836  genprndu  7837  ltpopr  7910  recexprlemm  7939  recexprlemopl  7940  recexprlemopu  7942  recexprlem1ssl  7948  recexprlem1ssu  7949  cauappcvgprlemupu  7964  caucvgprlemupu  7987  caucvgprprlemupu  8015  caucvgsrlemoffres  8115  map2psrprg  8120  resqrexlemgt0  11705  subcn2  11996  bezoutlembz  12700  pythagtriplem19  12980  mplsubgfileminv  14855  tgcl  14929  neiss  15015  ssnei2  15022  tgcnp  15074  cnptopco  15087  cnptopresti  15103  lmtopcnp  15115  blssexps  15294  blssex  15295  mopni3  15349  neibl  15356  metss  15359  metcnp3  15376  mpomulcn  15431  rescncf  15446  limcresi  15531  plyss  15603  umgrnloop0  16112  uhgr2edg  16201