Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximddv Structured version   Visualization version   GIF version

Theorem reximddv 3237
 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
StepHypRef Expression
1 reximddva.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
2 reximddva.1 . . . 4 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
32expr 460 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
43reximdva 3236 . 2 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  ∃wrex 3110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3114  df-rex 3115 This theorem is referenced by:  reximddv2  3240  dedekind  10796  caucvgrlem  15024  isprm5  16044  drsdirfi  17543  sylow2  18746  gexex  18969  nrmsep  21965  regsep2  21984  locfincmp  22134  dissnref  22136  met1stc  23131  xrge0tsms  23442  cnheibor  23563  lmcau  23920  ismbf3d  24261  ulmdvlem3  25000  legov  26382  legtrid  26388  midexlem  26489  opphllem  26532  mideulem  26533  midex  26534  oppperpex  26550  hpgid  26563  lnperpex  26600  trgcopy  26601  grpoidinv  28294  pjhthlem2  29178  mdsymlem3  30191  xrge0tsmsd  30745  ballotlemfc0  31858  ballotlemfcc  31859  cvmliftlem15  32653  unblimceq0  33954  knoppndvlem18  33976  lhpexle3lem  37300  lhpex2leN  37302  cdlemg1cex  37877  fsuppind  39443  nacsfix  39640  unxpwdom3  40026  rfcnnnub  41652  reximddv3  41775  climxrrelem  42378  climxrre  42379  xlimxrre  42460  stoweidlem27  42656
 Copyright terms: Public domain W3C validator