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 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  reximddv3  3150  reximddv2  3196  dedekind  11337  caucvgrlem  15639  isprm5  16677  drsdirfi  18266  sylow2  19556  gexex  19783  nrmsep  23244  regsep2  23263  locfincmp  23413  dissnref  23415  met1stc  24409  xrge0tsms  24723  cnheibor  24854  lmcau  25213  ismbf3d  25555  ulmdvlem3  26311  legov  28512  legtrid  28518  midexlem  28619  opphllem  28662  mideulem  28663  midex  28664  oppperpex  28680  hpgid  28693  lnperpex  28730  trgcopy  28731  grpoidinv  30437  pjhthlem2  31321  mdsymlem3  32334  xrge0tsmsd  33002  isdrng4  33245  drngidl  33404  ssdifidlprm  33429  qsdrngi  33466  ballotlemfc0  34484  ballotlemfcc  34485  cvmliftlem15  35285  unblimceq0  36495  knoppndvlem18  36517  lhpexle3lem  40005  lhpex2leN  40007  cdlemg1cex  40582  fsuppind  42578  nacsfix  42700  unxpwdom3  43084  rfcnnnub  45030  climxrrelem  45747  climxrre  45748  xlimxrre  45829  stoweidlem27  46025  thinciso  49459