Theorem reximddv 3178

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  reximddv3  3179  reximddv2  3221  dedekind  11476  caucvgrlem  15845  isprm5  16888  drsdirfi  18484  sylow2  19845  gexex  20072  isdrng4  20997  drngidl  21544  ssdifidlprm  21647  nrmsep  23680  regsep2  23699  locfincmp  23850  dissnref  23852  met1stc  24845  xrge0tsms  25159  cnheibor  25281  lmcau  25639  ismbf3d  25980  ulmdvlem3  26734  legov  29053  legtrid  29059  midexlem  29169  opphllem  29216  mideulem  29217  midex  29218  oppperpex  29234  hpgid  29249  lnperpex  29314  trgcopy  29316  grpoidinv  31115  pjhthlem2  31999  mdsymlem3  33012  xrge0tsmsd  33680  qsdrngi  34065  ballotlemfc0  35171  ballotlemfcc  35172  cvmliftlem15  36149  unblimceq0  37465  knoppndvlem18  37487  lhpexle3lem  41161  lhpex2leN  41163  cdlemg1cex  41738  fsuppind  43711  nacsfix  43816  unxpwdom3  44190  rfcnnnub  46146  climxrrelem  46852  climxrre  46853  xlimxrre  46934  stoweidlem27  47130  thinciso  50698