Theorem reximddv 3156

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  reximddv3  3157  reximddv2  3199  dedekind  11307  caucvgrlem  15633  isprm5  16675  drsdirfi  18269  sylow2  19599  gexex  19826  nrmsep  23347  regsep2  23366  locfincmp  23516  dissnref  23518  met1stc  24511  xrge0tsms  24825  cnheibor  24947  lmcau  25305  ismbf3d  25646  ulmdvlem3  26392  legov  28678  legtrid  28684  midexlem  28785  opphllem  28828  mideulem  28829  midex  28830  oppperpex  28846  hpgid  28859  lnperpex  28896  trgcopy  28897  grpoidinv  30604  pjhthlem2  31488  mdsymlem3  32501  xrge0tsmsd  33161  isdrng4  33386  drngidl  33523  ssdifidlprm  33548  qsdrngi  33585  ballotlemfc0  34684  ballotlemfcc  34685  cvmliftlem15  35533  unblimceq0  36820  knoppndvlem18  36842  lhpexle3lem  40510  lhpex2leN  40512  cdlemg1cex  41087  fsuppind  43047  nacsfix  43168  unxpwdom3  43547  rfcnnnub  45491  climxrrelem  46199  climxrre  46200  xlimxrre  46281  stoweidlem27  46477  thinciso  49967