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 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

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

This theorem is referenced by:  reximddv3  3182  reximddv2  3224  dedekind  11361  caucvgrlem  15714  isprm5  16756  drsdirfi  18351  sylow2  19687  gexex  19914  ssdifidlprm  21446  nrmsep  23475  regsep2  23494  locfincmp  23644  dissnref  23646  met1stc  24639  xrge0tsms  24953  cnheibor  25075  lmcau  25433  ismbf3d  25774  ulmdvlem3  26523  legov  28812  legtrid  28818  midexlem  28923  opphllem  28966  mideulem  28967  midex  28968  oppperpex  28984  hpgid  28997  lnperpex  29055  trgcopy  29056  grpoidinv  30769  pjhthlem2  31653  mdsymlem3  32666  xrge0tsmsd  33306  isdrng4  33531  drngidl  33657  qsdrngi  33694  ballotlemfc0  34800  ballotlemfcc  34801  cvmliftlem15  35661  unblimceq0  36958  knoppndvlem18  36980  lhpexle3lem  40647  lhpex2leN  40649  cdlemg1cex  41224  fsuppind  43184  nacsfix  43305  unxpwdom3  43684  rfcnnnub  45614  climxrrelem  46321  climxrre  46322  xlimxrre  46403  stoweidlem27  46599  thinciso  50099