Theorem reximddv 3177

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  reximddv3  3178  reximddv2  3220  dedekind  11343  caucvgrlem  15683  isprm5  16725  drsdirfi  18320  sylow2  19649  gexex  19876  nrmsep  23397  regsep2  23416  locfincmp  23566  dissnref  23568  met1stc  24561  xrge0tsms  24875  cnheibor  24997  lmcau  25355  ismbf3d  25696  ulmdvlem3  26442  legov  28731  legtrid  28737  midexlem  28838  opphllem  28881  mideulem  28882  midex  28883  oppperpex  28899  hpgid  28912  lnperpex  28949  trgcopy  28950  grpoidinv  30657  pjhthlem2  31541  mdsymlem3  32554  xrge0tsmsd  33214  isdrng4  33443  drngidl  33580  ssdifidlprm  33606  qsdrngi  33644  ballotlemfc0  34751  ballotlemfcc  34752  cvmliftlem15  35612  unblimceq0  36909  knoppndvlem18  36931  lhpexle3lem  40599  lhpex2leN  40601  cdlemg1cex  41176  fsuppind  43136  nacsfix  43257  unxpwdom3  43636  rfcnnnub  45580  climxrrelem  46287  climxrre  46288  xlimxrre  46369  stoweidlem27  46565  thinciso  50055