Theorem reximddv 3168

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  reximddv3  3169  reximddv2  3212  dedekind  11421  caucvgrlem  15705  isprm5  16740  drsdirfi  18362  sylow2  19658  gexex  19885  nrmsep  23380  regsep2  23399  locfincmp  23549  dissnref  23551  met1stc  24549  xrge0tsms  24869  cnheibor  25000  lmcau  25360  ismbf3d  25702  ulmdvlem3  26459  legov  28607  legtrid  28613  midexlem  28714  opphllem  28757  mideulem  28758  midex  28759  oppperpex  28775  hpgid  28788  lnperpex  28825  trgcopy  28826  grpoidinv  30536  pjhthlem2  31420  mdsymlem3  32433  xrge0tsmsd  33047  isdrng4  33278  drngidl  33440  ssdifidlprm  33465  qsdrngi  33502  ballotlemfc0  34473  ballotlemfcc  34474  cvmliftlem15  35282  unblimceq0  36489  knoppndvlem18  36511  lhpexle3lem  39993  lhpex2leN  39995  cdlemg1cex  40570  fsuppind  42576  nacsfix  42699  unxpwdom3  43083  rfcnnnub  44973  climxrrelem  45704  climxrre  45705  xlimxrre  45786  stoweidlem27  45982  thinciso  48860