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

Theorem reximddv 3014
 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 642 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
43reximdva 3013 . 2 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1987  ∃wrex 2909 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2913  df-rex 2914 This theorem is referenced by:  reximddv2  3015  dedekind  10160  caucvgrlem  14353  isprm5  15362  drsdirfi  16878  sylow2  17981  gexex  18196  nrmsep  21101  regsep2  21120  locfincmp  21269  dissnref  21271  met1stc  22266  xrge0tsms  22577  cnheibor  22694  lmcau  23051  ismbf3d  23361  ulmdvlem3  24094  legov  25414  legtrid  25420  midexlem  25521  opphllem  25561  mideulem  25562  midex  25563  oppperpex  25579  hpgid  25592  lnperpex  25629  trgcopy  25630  grpoidinv  27250  pjhthlem2  28139  mdsymlem3  29152  xrge0tsmsd  29612  ballotlemfc0  30377  ballotlemfcc  30378  cvmliftlem15  31041  unblimceq0  32193  knoppndvlem18  32215  lhpexle3lem  34816  lhpex2leN  34818  cdlemg1cex  35395  nacsfix  36794  unxpwdom3  37184  rfcnnnub  38717  stoweidlem27  39581
 Copyright terms: Public domain W3C validator