Theorem reximddv 3165

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-rex 3072

This theorem is referenced by:  reximddv2  3203  dedekind  11218  caucvgrlem  15463  isprm5  16489  drsdirfi  18100  sylow2  19307  gexex  19529  nrmsep  22591  regsep2  22610  locfincmp  22760  dissnref  22762  met1stc  23760  xrge0tsms  24080  cnheibor  24201  lmcau  24560  ismbf3d  24901  ulmdvlem3  25644  legov  27082  legtrid  27088  midexlem  27189  opphllem  27232  mideulem  27233  midex  27234  oppperpex  27250  hpgid  27263  lnperpex  27300  trgcopy  27301  grpoidinv  29006  pjhthlem2  29890  mdsymlem3  30903  xrge0tsmsd  31452  ballotlemfc0  32599  ballotlemfcc  32600  cvmliftlem15  33399  unblimceq0  34761  knoppndvlem18  34783  lhpexle3lem  38246  lhpex2leN  38248  cdlemg1cex  38823  fsuppind  40495  nacsfix  40750  unxpwdom3  41137  rfcnnnub  42813  reximddv3  42935  climxrrelem  43540  climxrre  43541  xlimxrre  43622  stoweidlem27  43818  thinciso  46606