Theorem reximddv 3204

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3070

This theorem is referenced by:  reximddv2  3207  dedekind  11138  caucvgrlem  15384  isprm5  16412  drsdirfi  18023  sylow2  19231  gexex  19454  nrmsep  22508  regsep2  22527  locfincmp  22677  dissnref  22679  met1stc  23677  xrge0tsms  23997  cnheibor  24118  lmcau  24477  ismbf3d  24818  ulmdvlem3  25561  legov  26946  legtrid  26952  midexlem  27053  opphllem  27096  mideulem  27097  midex  27098  oppperpex  27114  hpgid  27127  lnperpex  27164  trgcopy  27165  grpoidinv  28870  pjhthlem2  29754  mdsymlem3  30767  xrge0tsmsd  31317  ballotlemfc0  32459  ballotlemfcc  32460  cvmliftlem15  33260  unblimceq0  34687  knoppndvlem18  34709  lhpexle3lem  38025  lhpex2leN  38027  cdlemg1cex  38602  fsuppind  40279  nacsfix  40534  unxpwdom3  40920  rfcnnnub  42579  reximddv3  42700  climxrrelem  43290  climxrre  43291  xlimxrre  43372  stoweidlem27  43568  thinciso  46341