Theorem reximddv 3184

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093

This theorem is used by:  reximddv3  3185  reximddv2  3227  dedekind  11391  caucvgrlem  15750  isprm5  16791  drsdirfi  18386  sylow2  19727  gexex  19954  isdrng4  20876  drngidl  21422  ssdifidlprm  21523  nrmsep  23551  regsep2  23570  locfincmp  23720  dissnref  23722  met1stc  24715  xrge0tsms  25029  cnheibor  25151  lmcau  25509  ismbf3d  25850  ulmdvlem3  26602  legov  28891  legtrid  28897  midexlem  29006  opphllem  29053  mideulem  29054  midex  29055  oppperpex  29071  hpgid  29085  lnperpex  29150  trgcopy  29152  grpoidinv  30897  pjhthlem2  31781  mdsymlem3  32794  xrge0tsmsd  33424  qsdrngi  33808  ballotlemfc0  34915  ballotlemfcc  34916  cvmliftlem15  35811  unblimceq0  37137  knoppndvlem18  37159  lhpexle3lem  40826  lhpex2leN  40828  cdlemg1cex  41403  fsuppind  43363  nacsfix  43484  unxpwdom3  43863  rfcnnnub  45797  climxrrelem  46504  climxrre  46505  xlimxrre  46586  stoweidlem27  46782  thinciso  50289