Theorem reximddv 3148

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  reximddv3  3149  reximddv2  3191  dedekind  11276  caucvgrlem  15580  isprm5  16618  drsdirfi  18211  sylow2  19538  gexex  19765  nrmsep  23272  regsep2  23291  locfincmp  23441  dissnref  23443  met1stc  24436  xrge0tsms  24750  cnheibor  24881  lmcau  25240  ismbf3d  25582  ulmdvlem3  26338  legov  28563  legtrid  28569  midexlem  28670  opphllem  28713  mideulem  28714  midex  28715  oppperpex  28731  hpgid  28744  lnperpex  28781  trgcopy  28782  grpoidinv  30488  pjhthlem2  31372  mdsymlem3  32385  xrge0tsmsd  33042  isdrng4  33261  drngidl  33398  ssdifidlprm  33423  qsdrngi  33460  ballotlemfc0  34506  ballotlemfcc  34507  cvmliftlem15  35342  unblimceq0  36551  knoppndvlem18  36573  lhpexle3lem  40109  lhpex2leN  40111  cdlemg1cex  40686  fsuppind  42682  nacsfix  42804  unxpwdom3  43187  rfcnnnub  45132  climxrrelem  45846  climxrre  45847  xlimxrre  45928  stoweidlem27  46124  thinciso  49570