Theorem reximddv 3180

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  reximddv3  3181  reximddv2  3223  dedekind  11401  caucvgrlem  15764  isprm5  16804  drsdirfi  18399  sylow2  19759  gexex  19986  isdrng4  20908  drngidl  21454  ssdifidlprm  21555  nrmsep  23588  regsep2  23607  locfincmp  23758  dissnref  23760  met1stc  24753  xrge0tsms  25067  cnheibor  25189  lmcau  25547  ismbf3d  25888  ulmdvlem3  26645  legov  28935  legtrid  28941  midexlem  29051  opphllem  29098  mideulem  29099  midex  29100  oppperpex  29116  hpgid  29131  lnperpex  29196  trgcopy  29198  grpoidinv  30997  pjhthlem2  31881  mdsymlem3  32894  xrge0tsmsd  33521  qsdrngi  33905  ballotlemfc0  35012  ballotlemfcc  35013  cvmliftlem15  35885  unblimceq0  37212  knoppndvlem18  37234  lhpexle3lem  40892  lhpex2leN  40894  cdlemg1cex  41469  fsuppind  43444  nacsfix  43565  unxpwdom3  43944  rfcnnnub  45878  climxrrelem  46585  climxrre  46586  xlimxrre  46667  stoweidlem27  46863  thinciso  50404