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

Theorem reximddv 3198
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 449 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
43reximdva 3197 . 2 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wcel 2157  wrex 3090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-ral 3094  df-rex 3095
This theorem is referenced by:  reximddv2  3201  dedekind  10490  caucvgrlem  14744  isprm5  15752  drsdirfi  17253  sylow2  18354  gexex  18571  nrmsep  21490  regsep2  21509  locfincmp  21658  dissnref  21660  met1stc  22654  xrge0tsms  22965  cnheibor  23082  lmcau  23439  ismbf3d  23762  ulmdvlem3  24497  legov  25836  legtrid  25842  midexlem  25943  opphllem  25983  mideulem  25984  midex  25985  oppperpex  26001  hpgid  26014  lnperpex  26051  trgcopy  26052  grpoidinv  27888  pjhthlem2  28776  mdsymlem3  29789  xrge0tsmsd  30301  ballotlemfc0  31071  ballotlemfcc  31072  cvmliftlem15  31797  unblimceq0  33006  knoppndvlem18  33028  lhpexle3lem  36032  lhpex2leN  36034  cdlemg1cex  36609  nacsfix  38057  unxpwdom3  38446  rfcnnnub  39951  reximddv3  40094  climxrrelem  40721  climxrre  40722  xlimxrre  40797  stoweidlem27  40983
  Copyright terms: Public domain W3C validator