Theorem reximddv 3177

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  reximddv3  3178  reximddv2  3221  dedekind  11453  caucvgrlem  15721  isprm5  16754  drsdirfi  18375  sylow2  19668  gexex  19895  nrmsep  23386  regsep2  23405  locfincmp  23555  dissnref  23557  met1stc  24555  xrge0tsms  24875  cnheibor  25006  lmcau  25366  ismbf3d  25708  ulmdvlem3  26463  legov  28611  legtrid  28617  midexlem  28718  opphllem  28761  mideulem  28762  midex  28763  oppperpex  28779  hpgid  28792  lnperpex  28829  trgcopy  28830  grpoidinv  30540  pjhthlem2  31424  mdsymlem3  32437  xrge0tsmsd  33041  isdrng4  33264  drngidl  33426  ssdifidlprm  33451  qsdrngi  33488  ballotlemfc0  34457  ballotlemfcc  34458  cvmliftlem15  35266  unblimceq0  36473  knoppndvlem18  36495  lhpexle3lem  39968  lhpex2leN  39970  cdlemg1cex  40545  fsuppind  42545  nacsfix  42668  unxpwdom3  43052  rfcnnnub  44936  climxrrelem  45670  climxrre  45671  xlimxrre  45752  stoweidlem27  45948  thinciso  48727