Theorem reximddv 3170

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3069

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 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  reximddv2  3211  dedekind  11382  caucvgrlem  15624  isprm5  16649  drsdirfi  18263  sylow2  19536  gexex  19763  nrmsep  23082  regsep2  23101  locfincmp  23251  dissnref  23253  met1stc  24251  xrge0tsms  24571  cnheibor  24702  lmcau  25062  ismbf3d  25404  ulmdvlem3  26147  legov  28100  legtrid  28106  midexlem  28207  opphllem  28250  mideulem  28251  midex  28252  oppperpex  28268  hpgid  28281  lnperpex  28318  trgcopy  28319  grpoidinv  30025  pjhthlem2  30909  mdsymlem3  31922  xrge0tsmsd  32476  isdrng4  32662  drngidl  32822  qsdrngi  32880  ballotlemfc0  33786  ballotlemfcc  33787  cvmliftlem15  34584  unblimceq0  35687  knoppndvlem18  35709  lhpexle3lem  39186  lhpex2leN  39188  cdlemg1cex  39763  fsuppind  41465  nacsfix  41753  unxpwdom3  42140  rfcnnnub  44023  reximddv3  44143  climxrrelem  44765  climxrre  44766  xlimxrre  44847  stoweidlem27  45043  thinciso  47769