Theorem reximddv 3235

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2079  ∃wrex 3104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-ral 3108  df-rex 3109

This theorem is referenced by:  reximddv2  3238  dedekind  10639  caucvgrlem  14851  isprm5  15868  drsdirfi  17365  sylow2  18469  gexex  18684  nrmsep  21637  regsep2  21656  locfincmp  21806  dissnref  21808  met1stc  22802  xrge0tsms  23113  cnheibor  23230  lmcau  23587  ismbf3d  23926  ulmdvlem3  24661  legov  26041  legtrid  26047  midexlem  26148  opphllem  26191  mideulem  26192  midex  26193  oppperpex  26209  hpgid  26222  lnperpex  26259  trgcopy  26260  grpoidinv  27964  pjhthlem2  28848  mdsymlem3  29861  xrge0tsmsd  30460  ballotlemfc0  31323  ballotlemfcc  31324  cvmliftlem15  32109  unblimceq0  33399  knoppndvlem18  33421  lhpexle3lem  36628  lhpex2leN  36630  cdlemg1cex  37205  nacsfix  38744  unxpwdom3  39131  rfcnnnub  40784  reximddv3  40912  climxrrelem  41526  climxrre  41527  xlimxrre  41608  stoweidlem27  41808