Theorem reximddv 3172

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  reximddv2  3213  dedekind  11377  caucvgrlem  15619  isprm5  16644  drsdirfi  18258  sylow2  19494  gexex  19721  nrmsep  22861  regsep2  22880  locfincmp  23030  dissnref  23032  met1stc  24030  xrge0tsms  24350  cnheibor  24471  lmcau  24830  ismbf3d  25171  ulmdvlem3  25914  legov  27836  legtrid  27842  midexlem  27943  opphllem  27986  mideulem  27987  midex  27988  oppperpex  28004  hpgid  28017  lnperpex  28054  trgcopy  28055  grpoidinv  29761  pjhthlem2  30645  mdsymlem3  31658  xrge0tsmsd  32209  isdrng4  32395  drngidl  32551  qsdrngi  32609  ballotlemfc0  33491  ballotlemfcc  33492  cvmliftlem15  34289  unblimceq0  35383  knoppndvlem18  35405  lhpexle3lem  38882  lhpex2leN  38884  cdlemg1cex  39459  fsuppind  41162  nacsfix  41450  unxpwdom3  41837  rfcnnnub  43720  reximddv3  43840  climxrrelem  44465  climxrre  44466  xlimxrre  44547  stoweidlem27  44743  thinciso  47680