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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  ∃wrex 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3056  df-rex 3057

This theorem is referenced by:  reximddv2  3187  dedekind  10960  caucvgrlem  15201  isprm5  16227  drsdirfi  17766  sylow2  18969  gexex  19192  nrmsep  22208  regsep2  22227  locfincmp  22377  dissnref  22379  met1stc  23373  xrge0tsms  23685  cnheibor  23806  lmcau  24164  ismbf3d  24505  ulmdvlem3  25248  legov  26630  legtrid  26636  midexlem  26737  opphllem  26780  mideulem  26781  midex  26782  oppperpex  26798  hpgid  26811  lnperpex  26848  trgcopy  26849  grpoidinv  28543  pjhthlem2  29427  mdsymlem3  30440  xrge0tsmsd  30990  ballotlemfc0  32125  ballotlemfcc  32126  cvmliftlem15  32927  unblimceq0  34373  knoppndvlem18  34395  lhpexle3lem  37711  lhpex2leN  37713  cdlemg1cex  38288  fsuppind  39930  nacsfix  40178  unxpwdom3  40564  rfcnnnub  42193  reximddv3  42314  climxrrelem  42908  climxrre  42909  xlimxrre  42990  stoweidlem27  43186  thinciso  45957