Theorem reximddv 3156

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3060

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 3061

This theorem is referenced by:  reximddv3  3157  reximddv2  3200  dedekind  11398  caucvgrlem  15689  isprm5  16726  drsdirfi  18317  sylow2  19607  gexex  19834  nrmsep  23295  regsep2  23314  locfincmp  23464  dissnref  23466  met1stc  24460  xrge0tsms  24774  cnheibor  24905  lmcau  25265  ismbf3d  25607  ulmdvlem3  26363  legov  28564  legtrid  28570  midexlem  28671  opphllem  28714  mideulem  28715  midex  28716  oppperpex  28732  hpgid  28745  lnperpex  28782  trgcopy  28783  grpoidinv  30489  pjhthlem2  31373  mdsymlem3  32386  xrge0tsmsd  33056  isdrng4  33289  drngidl  33448  ssdifidlprm  33473  qsdrngi  33510  ballotlemfc0  34525  ballotlemfcc  34526  cvmliftlem15  35320  unblimceq0  36525  knoppndvlem18  36547  lhpexle3lem  40030  lhpex2leN  40032  cdlemg1cex  40607  fsuppind  42613  nacsfix  42735  unxpwdom3  43119  rfcnnnub  45060  climxrrelem  45778  climxrre  45779  xlimxrre  45860  stoweidlem27  46056  thinciso  49356