Theorem reximddv 3277

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  reximddv2  3280  dedekind  10805  caucvgrlem  15031  isprm5  16053  drsdirfi  17550  sylow2  18753  gexex  18975  nrmsep  21967  regsep2  21986  locfincmp  22136  dissnref  22138  met1stc  23133  xrge0tsms  23444  cnheibor  23561  lmcau  23918  ismbf3d  24257  ulmdvlem3  24992  legov  26373  legtrid  26379  midexlem  26480  opphllem  26523  mideulem  26524  midex  26525  oppperpex  26541  hpgid  26554  lnperpex  26591  trgcopy  26592  grpoidinv  28287  pjhthlem2  29171  mdsymlem3  30184  xrge0tsmsd  30694  ballotlemfc0  31752  ballotlemfcc  31753  cvmliftlem15  32547  unblimceq0  33848  knoppndvlem18  33870  lhpexle3lem  37149  lhpex2leN  37151  cdlemg1cex  37726  nacsfix  39316  unxpwdom3  39702  rfcnnnub  41300  reximddv3  41427  climxrrelem  42037  climxrre  42038  xlimxrre  42119  stoweidlem27  42319