Theorem reximddv 3149

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

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

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 3058

This theorem is referenced by:  reximddv3  3150  reximddv2  3192  dedekind  11283  caucvgrlem  15582  isprm5  16620  drsdirfi  18213  sylow2  19540  gexex  19767  nrmsep  23273  regsep2  23292  locfincmp  23442  dissnref  23444  met1stc  24437  xrge0tsms  24751  cnheibor  24882  lmcau  25241  ismbf3d  25583  ulmdvlem3  26339  legov  28564  legtrid  28570  midexlem  28671  opphllem  28714  mideulem  28715  midex  28716  oppperpex  28732  hpgid  28745  lnperpex  28782  trgcopy  28783  grpoidinv  30490  pjhthlem2  31374  mdsymlem3  32387  xrge0tsmsd  33049  isdrng4  33268  drngidl  33405  ssdifidlprm  33430  qsdrngi  33467  ballotlemfc0  34527  ballotlemfcc  34528  cvmliftlem15  35363  unblimceq0  36572  knoppndvlem18  36594  lhpexle3lem  40131  lhpex2leN  40133  cdlemg1cex  40708  fsuppind  42709  nacsfix  42830  unxpwdom3  43213  rfcnnnub  45158  climxrrelem  45872  climxrre  45873  xlimxrre  45954  stoweidlem27  46150  thinciso  49596