Theorem reximddv 3154

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  reximddv3  3155  reximddv2  3197  dedekind  11308  caucvgrlem  15608  isprm5  16646  drsdirfi  18240  sylow2  19567  gexex  19794  nrmsep  23313  regsep2  23332  locfincmp  23482  dissnref  23484  met1stc  24477  xrge0tsms  24791  cnheibor  24922  lmcau  25281  ismbf3d  25623  ulmdvlem3  26379  legov  28669  legtrid  28675  midexlem  28776  opphllem  28819  mideulem  28820  midex  28821  oppperpex  28837  hpgid  28850  lnperpex  28887  trgcopy  28888  grpoidinv  30595  pjhthlem2  31479  mdsymlem3  32492  xrge0tsmsd  33166  isdrng4  33388  drngidl  33525  ssdifidlprm  33550  qsdrngi  33587  ballotlemfc0  34670  ballotlemfcc  34671  cvmliftlem15  35511  unblimceq0  36726  knoppndvlem18  36748  lhpexle3lem  40384  lhpex2leN  40386  cdlemg1cex  40961  fsuppind  42945  nacsfix  43066  unxpwdom3  43449  rfcnnnub  45393  climxrrelem  46104  climxrre  46105  xlimxrre  46186  stoweidlem27  46382  thinciso  49826