Theorem reximddv 3179

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

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

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 3088

This theorem is used by:  reximddv3  3180  reximddv2  3222  dedekind  11454  caucvgrlem  15820  isprm5  16863  drsdirfi  18459  sylow2  19820  gexex  20047  isdrng4  20972  drngidl  21519  ssdifidlprm  21622  nrmsep  23655  regsep2  23674  locfincmp  23825  dissnref  23827  met1stc  24820  xrge0tsms  25134  cnheibor  25256  lmcau  25614  ismbf3d  25955  ulmdvlem3  26711  legov  29030  legtrid  29036  midexlem  29146  opphllem  29193  mideulem  29194  midex  29195  oppperpex  29211  hpgid  29226  lnperpex  29291  trgcopy  29293  grpoidinv  31092  pjhthlem2  31976  mdsymlem3  32989  xrge0tsmsd  33616  qsdrngi  34001  ballotlemfc0  35108  ballotlemfcc  35109  cvmliftlem15  36032  unblimceq0  37343  knoppndvlem18  37365  lhpexle3lem  41036  lhpex2leN  41038  cdlemg1cex  41613  fsuppind  43580  nacsfix  43676  unxpwdom3  44055  rfcnnnub  45996  climxrrelem  46703  climxrre  46704  xlimxrre  46785  stoweidlem27  46981  thinciso  50522