Theorem reximddv 3150

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  reximddv3  3151  reximddv2  3197  dedekind  11344  caucvgrlem  15646  isprm5  16684  drsdirfi  18273  sylow2  19563  gexex  19790  nrmsep  23251  regsep2  23270  locfincmp  23420  dissnref  23422  met1stc  24416  xrge0tsms  24730  cnheibor  24861  lmcau  25220  ismbf3d  25562  ulmdvlem3  26318  legov  28519  legtrid  28525  midexlem  28626  opphllem  28669  mideulem  28670  midex  28671  oppperpex  28687  hpgid  28700  lnperpex  28737  trgcopy  28738  grpoidinv  30444  pjhthlem2  31328  mdsymlem3  32341  xrge0tsmsd  33009  isdrng4  33252  drngidl  33411  ssdifidlprm  33436  qsdrngi  33473  ballotlemfc0  34491  ballotlemfcc  34492  cvmliftlem15  35292  unblimceq0  36502  knoppndvlem18  36524  lhpexle3lem  40012  lhpex2leN  40014  cdlemg1cex  40589  fsuppind  42585  nacsfix  42707  unxpwdom3  43091  rfcnnnub  45037  climxrrelem  45754  climxrre  45755  xlimxrre  45836  stoweidlem27  46032  thinciso  49463