Theorem reximddv 3198

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

Syntax hints:   → wi 4   ∧ wa 385   ∈ wcel 2157  ∃wrex 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-ral 3094  df-rex 3095

This theorem is referenced by:  reximddv2  3201  dedekind  10490  caucvgrlem  14744  isprm5  15752  drsdirfi  17253  sylow2  18354  gexex  18571  nrmsep  21490  regsep2  21509  locfincmp  21658  dissnref  21660  met1stc  22654  xrge0tsms  22965  cnheibor  23082  lmcau  23439  ismbf3d  23762  ulmdvlem3  24497  legov  25836  legtrid  25842  midexlem  25943  opphllem  25983  mideulem  25984  midex  25985  oppperpex  26001  hpgid  26014  lnperpex  26051  trgcopy  26052  grpoidinv  27888  pjhthlem2  28776  mdsymlem3  29789  xrge0tsmsd  30301  ballotlemfc0  31071  ballotlemfcc  31072  cvmliftlem15  31797  unblimceq0  33006  knoppndvlem18  33028  lhpexle3lem  36032  lhpex2leN  36034  cdlemg1cex  36609  nacsfix  38057  unxpwdom3  38446  rfcnnnub  39951  reximddv3  40094  climxrrelem  40721  climxrre  40722  xlimxrre  40797  stoweidlem27  40983