Theorem reximddv 3181

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  reximddv3  3182  reximddv2  3224  dedekind  11374  caucvgrlem  15726  isprm5  16767  drsdirfi  18362  sylow2  19697  gexex  19924  isdrng4  20826  drngidl  21366  ssdifidlprm  21467  nrmsep  23495  regsep2  23514  locfincmp  23664  dissnref  23666  met1stc  24659  xrge0tsms  24973  cnheibor  25095  lmcau  25453  ismbf3d  25794  ulmdvlem3  26546  legov  28835  legtrid  28841  midexlem  28950  opphllem  28997  mideulem  28998  midex  28999  oppperpex  29015  hpgid  29029  lnperpex  29094  trgcopy  29096  grpoidinv  30841  pjhthlem2  31725  mdsymlem3  32738  xrge0tsmsd  33374  qsdrngi  33758  ballotlemfc0  34864  ballotlemfcc  34865  cvmliftlem15  35771  unblimceq0  37077  knoppndvlem18  37099  lhpexle3lem  40766  lhpex2leN  40768  cdlemg1cex  41343  fsuppind  43305  nacsfix  43426  unxpwdom3  43805  rfcnnnub  45739  climxrrelem  46446  climxrre  46447  xlimxrre  46528  stoweidlem27  46724  thinciso  50231