Theorem reximddv 3145

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  reximddv3  3146  reximddv2  3188  dedekind  11297  caucvgrlem  15598  isprm5  16636  drsdirfi  18229  sylow2  19523  gexex  19750  nrmsep  23260  regsep2  23279  locfincmp  23429  dissnref  23431  met1stc  24425  xrge0tsms  24739  cnheibor  24870  lmcau  25229  ismbf3d  25571  ulmdvlem3  26327  legov  28548  legtrid  28554  midexlem  28655  opphllem  28698  mideulem  28699  midex  28700  oppperpex  28716  hpgid  28729  lnperpex  28766  trgcopy  28767  grpoidinv  30470  pjhthlem2  31354  mdsymlem3  32367  xrge0tsmsd  33028  isdrng4  33247  drngidl  33383  ssdifidlprm  33408  qsdrngi  33445  ballotlemfc0  34463  ballotlemfcc  34464  cvmliftlem15  35273  unblimceq0  36483  knoppndvlem18  36505  lhpexle3lem  39993  lhpex2leN  39995  cdlemg1cex  40570  fsuppind  42566  nacsfix  42688  unxpwdom3  43071  rfcnnnub  45017  climxrrelem  45734  climxrre  45735  xlimxrre  45816  stoweidlem27  46012  thinciso  49459