Theorem reximddv 3001

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  reximddv2  3002  dedekind  10079  caucvgrlem  14251  isprm5  15257  drsdirfi  16761  sylow2  17864  gexex  18079  nrmsep  20971  regsep2  20990  locfincmp  21139  dissnref  21141  met1stc  22136  xrge0tsms  22445  cnheibor  22562  lmcau  22919  ismbf3d  23227  ulmdvlem3  23960  legov  25280  legtrid  25286  midexlem  25387  opphllem  25427  mideulem  25428  midex  25429  oppperpex  25445  hpgid  25458  lnperpex  25495  trgcopy  25496  grpoidinv  26746  pjhthlem2  27635  mdsymlem3  28648  xrge0tsmsd  29116  ballotlemfc0  29881  ballotlemfcc  29882  cvmliftlem15  30534  unblimceq0  31668  knoppndvlem18  31690  lhpexle3lem  34315  lhpex2leN  34317  cdlemg1cex  34894  nacsfix  36293  unxpwdom3  36683  rfcnnnub  38218  stoweidlem27  38920