Theorem reximddv 3153

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  reximddv3  3154  reximddv2  3196  dedekind  11309  caucvgrlem  15635  isprm5  16677  drsdirfi  18271  sylow2  19601  gexex  19828  nrmsep  23322  regsep2  23341  locfincmp  23491  dissnref  23493  met1stc  24486  xrge0tsms  24800  cnheibor  24922  lmcau  25280  ismbf3d  25621  ulmdvlem3  26367  legov  28653  legtrid  28659  midexlem  28760  opphllem  28803  mideulem  28804  midex  28805  oppperpex  28821  hpgid  28834  lnperpex  28871  trgcopy  28872  grpoidinv  30579  pjhthlem2  31463  mdsymlem3  32476  xrge0tsmsd  33134  isdrng4  33356  drngidl  33493  ssdifidlprm  33518  qsdrngi  33555  ballotlemfc0  34637  ballotlemfcc  34638  cvmliftlem15  35480  unblimceq0  36767  knoppndvlem18  36789  lhpexle3lem  40457  lhpex2leN  40459  cdlemg1cex  41034  fsuppind  43023  nacsfix  43144  unxpwdom3  43523  rfcnnnub  45467  climxrrelem  46177  climxrre  46178  xlimxrre  46259  stoweidlem27  46455  thinciso  49945