Theorem reximddv 3152

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

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 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  reximddv3  3153  reximddv2  3195  dedekind  11296  caucvgrlem  15596  isprm5  16634  drsdirfi  18228  sylow2  19555  gexex  19782  nrmsep  23301  regsep2  23320  locfincmp  23470  dissnref  23472  met1stc  24465  xrge0tsms  24779  cnheibor  24910  lmcau  25269  ismbf3d  25611  ulmdvlem3  26367  legov  28657  legtrid  28663  midexlem  28764  opphllem  28807  mideulem  28808  midex  28809  oppperpex  28825  hpgid  28838  lnperpex  28875  trgcopy  28876  grpoidinv  30583  pjhthlem2  31467  mdsymlem3  32480  xrge0tsmsd  33155  isdrng4  33377  drngidl  33514  ssdifidlprm  33539  qsdrngi  33576  ballotlemfc0  34650  ballotlemfcc  34651  cvmliftlem15  35492  unblimceq0  36707  knoppndvlem18  36729  lhpexle3lem  40271  lhpex2leN  40273  cdlemg1cex  40848  fsuppind  42833  nacsfix  42954  unxpwdom3  43337  rfcnnnub  45281  climxrrelem  45993  climxrre  45994  xlimxrre  46075  stoweidlem27  46271  thinciso  49715