Theorem reximddv 3171

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)

Hypotheses

Ref	Expression
reximddva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
reximddva.2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Assertion

Ref	Expression
reximddv	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximddv

Step	Hyp	Ref	Expression
1		reximddva.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
2		reximddva.1	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
3	2	expr 457	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
4	3	reximdva 3168	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  reximddv2  3212  dedekind  11379  caucvgrlem  15621  isprm5  16646  drsdirfi  18260  sylow2  19496  gexex  19723  nrmsep  22868  regsep2  22887  locfincmp  23037  dissnref  23039  met1stc  24037  xrge0tsms  24357  cnheibor  24478  lmcau  24837  ismbf3d  25178  ulmdvlem3  25921  legov  27874  legtrid  27880  midexlem  27981  opphllem  28024  mideulem  28025  midex  28026  oppperpex  28042  hpgid  28055  lnperpex  28092  trgcopy  28093  grpoidinv  29799  pjhthlem2  30683  mdsymlem3  31696  xrge0tsmsd  32250  isdrng4  32436  drngidl  32596  qsdrngi  32654  ballotlemfc0  33560  ballotlemfcc  33561  cvmliftlem15  34358  unblimceq0  35469  knoppndvlem18  35491  lhpexle3lem  38968  lhpex2leN  38970  cdlemg1cex  39545  fsuppind  41244  nacsfix  41532  unxpwdom3  41919  rfcnnnub  43802  reximddv3  43922  climxrrelem  44544  climxrre  44545  xlimxrre  44626  stoweidlem27  44822  thinciso  47758