Theorem reximddv 3182

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  reximddv3  3183  reximddv2  3225  dedekind  11500  caucvgrlem  15869  isprm5  16912  drsdirfi  18508  sylow2  19870  gexex  20097  isdrng4  21022  drngidl  21569  ssdifidlprm  21672  nrmsep  23705  regsep2  23724  locfincmp  23875  dissnref  23877  met1stc  24870  xrge0tsms  25184  cnheibor  25306  lmcau  25664  ismbf3d  26005  ulmdvlem3  26759  legov  29078  legtrid  29084  midexlem  29194  opphllem  29241  mideulem  29242  midex  29243  oppperpex  29259  hpgid  29274  lnperpex  29339  trgcopy  29341  grpoidinv  31140  pjhthlem2  32024  mdsymlem3  33037  xrge0tsmsd  33704  qsdrngi  34089  ballotlemfc0  35195  ballotlemfcc  35196  cvmliftlem15  36230  unblimceq0  37551  knoppndvlem18  37573  lhpexle3lem  41260  lhpex2leN  41262  cdlemg1cex  41837  fsuppind  43811  nacsfix  43916  unxpwdom3  44290  rfcnnnub  46258  climxrrelem  46964  climxrre  46965  xlimxrre  47046  stoweidlem27  47242  thinciso  50810