Theorem reximddv 3154

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

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

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 3063

This theorem is referenced by:  reximddv3  3155  reximddv2  3197  dedekind  11300  caucvgrlem  15626  isprm5  16668  drsdirfi  18262  sylow2  19592  gexex  19819  nrmsep  23332  regsep2  23351  locfincmp  23501  dissnref  23503  met1stc  24496  xrge0tsms  24810  cnheibor  24932  lmcau  25290  ismbf3d  25631  ulmdvlem3  26380  legov  28667  legtrid  28673  midexlem  28774  opphllem  28817  mideulem  28818  midex  28819  oppperpex  28835  hpgid  28848  lnperpex  28885  trgcopy  28886  grpoidinv  30594  pjhthlem2  31478  mdsymlem3  32491  xrge0tsmsd  33149  isdrng4  33371  drngidl  33508  ssdifidlprm  33533  qsdrngi  33570  ballotlemfc0  34653  ballotlemfcc  34654  cvmliftlem15  35496  unblimceq0  36783  knoppndvlem18  36805  lhpexle3lem  40471  lhpex2leN  40473  cdlemg1cex  41048  fsuppind  43037  nacsfix  43158  unxpwdom3  43541  rfcnnnub  45485  climxrrelem  46195  climxrre  46196  xlimxrre  46277  stoweidlem27  46473  thinciso  49957