Theorem reximddv 3187

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 461	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
4	3	reximdva 3184	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
5	1, 4	mpd 16	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  reximddv3  3188  reximddv2  3230  dedekind  11369  caucvgrlem  15720  isprm5  16762  drsdirfi  18357  sylow2  19692  gexex  19919  ssdifidlprm  21451  nrmsep  23479  regsep2  23498  locfincmp  23648  dissnref  23650  met1stc  24643  xrge0tsms  24957  cnheibor  25079  lmcau  25437  ismbf3d  25778  ulmdvlem3  26527  legov  28816  legtrid  28822  midexlem  28927  opphllem  28971  mideulem  28972  midex  28973  oppperpex  28989  hpgid  29003  lnperpex  29066  trgcopy  29068  grpoidinv  30797  pjhthlem2  31681  mdsymlem3  32694  xrge0tsmsd  33330  isdrng4  33555  drngidl  33681  qsdrngi  33718  ballotlemfc0  34824  ballotlemfcc  34825  cvmliftlem15  35685  unblimceq0  36981  knoppndvlem18  37003  lhpexle3lem  40670  lhpex2leN  40672  cdlemg1cex  41247  fsuppind  43207  nacsfix  43328  unxpwdom3  43707  rfcnnnub  45641  climxrrelem  46348  climxrre  46349  xlimxrre  46430  stoweidlem27  46626  thinciso  50126