Theorem reximddv 3171

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  reximddv3  3172  reximddv2  3215  dedekind  11424  caucvgrlem  15709  isprm5  16744  drsdirfi  18351  sylow2  19644  gexex  19871  nrmsep  23365  regsep2  23384  locfincmp  23534  dissnref  23536  met1stc  24534  xrge0tsms  24856  cnheibor  24987  lmcau  25347  ismbf3d  25689  ulmdvlem3  26445  legov  28593  legtrid  28599  midexlem  28700  opphllem  28743  mideulem  28744  midex  28745  oppperpex  28761  hpgid  28774  lnperpex  28811  trgcopy  28812  grpoidinv  30527  pjhthlem2  31411  mdsymlem3  32424  xrge0tsmsd  33065  isdrng4  33298  drngidl  33461  ssdifidlprm  33486  qsdrngi  33523  ballotlemfc0  34495  ballotlemfcc  34496  cvmliftlem15  35303  unblimceq0  36508  knoppndvlem18  36530  lhpexle3lem  40013  lhpex2leN  40015  cdlemg1cex  40590  fsuppind  42600  nacsfix  42723  unxpwdom3  43107  rfcnnnub  45041  climxrrelem  45764  climxrre  45765  xlimxrre  45846  stoweidlem27  46042  thinciso  49117