Theorem reximddv 3148

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 456	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
4	3	reximdva 3145	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  reximddv3  3149  reximddv2  3191  dedekind  11276  caucvgrlem  15580  isprm5  16618  drsdirfi  18211  sylow2  19539  gexex  19766  nrmsep  23273  regsep2  23292  locfincmp  23442  dissnref  23444  met1stc  24437  xrge0tsms  24751  cnheibor  24882  lmcau  25241  ismbf3d  25583  ulmdvlem3  26339  legov  28564  legtrid  28570  midexlem  28671  opphllem  28714  mideulem  28715  midex  28716  oppperpex  28732  hpgid  28745  lnperpex  28782  trgcopy  28783  grpoidinv  30486  pjhthlem2  31370  mdsymlem3  32383  xrge0tsmsd  33040  isdrng4  33259  drngidl  33396  ssdifidlprm  33421  qsdrngi  33458  ballotlemfc0  34504  ballotlemfcc  34505  cvmliftlem15  35340  unblimceq0  36547  knoppndvlem18  36569  lhpexle3lem  40056  lhpex2leN  40058  cdlemg1cex  40633  fsuppind  42629  nacsfix  42751  unxpwdom3  43134  rfcnnnub  45079  climxrrelem  45793  climxrre  45794  xlimxrre  45875  stoweidlem27  46071  thinciso  49508