Theorem reximddv 3203

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  reximddv2  3206  dedekind  11068  caucvgrlem  15312  isprm5  16340  drsdirfi  17938  sylow2  19146  gexex  19369  nrmsep  22416  regsep2  22435  locfincmp  22585  dissnref  22587  met1stc  23583  xrge0tsms  23903  cnheibor  24024  lmcau  24382  ismbf3d  24723  ulmdvlem3  25466  legov  26850  legtrid  26856  midexlem  26957  opphllem  27000  mideulem  27001  midex  27002  oppperpex  27018  hpgid  27031  lnperpex  27068  trgcopy  27069  grpoidinv  28771  pjhthlem2  29655  mdsymlem3  30668  xrge0tsmsd  31219  ballotlemfc0  32359  ballotlemfcc  32360  cvmliftlem15  33160  unblimceq0  34614  knoppndvlem18  34636  lhpexle3lem  37952  lhpex2leN  37954  cdlemg1cex  38529  fsuppind  40202  nacsfix  40450  unxpwdom3  40836  rfcnnnub  42468  reximddv3  42589  climxrrelem  43180  climxrre  43181  xlimxrre  43262  stoweidlem27  43458  thinciso  46229