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

Theorem reximddv 3235
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 457 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
43reximdva 3234 . 2 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2079  wrex 3104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-ral 3108  df-rex 3109
This theorem is referenced by:  reximddv2  3238  dedekind  10639  caucvgrlem  14851  isprm5  15868  drsdirfi  17365  sylow2  18469  gexex  18684  nrmsep  21637  regsep2  21656  locfincmp  21806  dissnref  21808  met1stc  22802  xrge0tsms  23113  cnheibor  23230  lmcau  23587  ismbf3d  23926  ulmdvlem3  24661  legov  26041  legtrid  26047  midexlem  26148  opphllem  26191  mideulem  26192  midex  26193  oppperpex  26209  hpgid  26222  lnperpex  26259  trgcopy  26260  grpoidinv  27964  pjhthlem2  28848  mdsymlem3  29861  xrge0tsmsd  30460  ballotlemfc0  31323  ballotlemfcc  31324  cvmliftlem15  32109  unblimceq0  33399  knoppndvlem18  33421  lhpexle3lem  36628  lhpex2leN  36630  cdlemg1cex  37205  nacsfix  38744  unxpwdom3  39131  rfcnnnub  40784  reximddv3  40912  climxrrelem  41526  climxrre  41527  xlimxrre  41608  stoweidlem27  41808
  Copyright terms: Public domain W3C validator