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

Theorem reximddv 3157
 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 644 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
43reximdva 3156 . 2 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2140  ∃wrex 3052 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-ral 3056  df-rex 3057 This theorem is referenced by:  reximddv2  3159  dedekind  10413  caucvgrlem  14623  isprm5  15642  drsdirfi  17160  sylow2  18262  gexex  18477  nrmsep  21384  regsep2  21403  locfincmp  21552  dissnref  21554  met1stc  22548  xrge0tsms  22859  cnheibor  22976  lmcau  23332  ismbf3d  23641  ulmdvlem3  24376  legov  25701  legtrid  25707  midexlem  25808  opphllem  25848  mideulem  25849  midex  25850  oppperpex  25866  hpgid  25879  lnperpex  25916  trgcopy  25917  grpoidinv  27693  pjhthlem2  28582  mdsymlem3  29595  xrge0tsmsd  30116  ballotlemfc0  30885  ballotlemfcc  30886  cvmliftlem15  31609  unblimceq0  32826  knoppndvlem18  32848  lhpexle3lem  35819  lhpex2leN  35821  cdlemg1cex  36397  nacsfix  37796  unxpwdom3  38186  rfcnnnub  39713  reximddv3  39861  climxrrelem  40503  climxrre  40504  xlimxrre  40579  stoweidlem27  40766
 Copyright terms: Public domain W3C validator