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

Theorem reximddv 3171
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 456 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
43reximdva 3168 . 2 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071
This theorem is referenced by:  reximddv3  3172  reximddv2  3215  dedekind  11424  caucvgrlem  15709  isprm5  16744  drsdirfi  18351  sylow2  19644  gexex  19871  nrmsep  23365  regsep2  23384  locfincmp  23534  dissnref  23536  met1stc  24534  xrge0tsms  24856  cnheibor  24987  lmcau  25347  ismbf3d  25689  ulmdvlem3  26445  legov  28593  legtrid  28599  midexlem  28700  opphllem  28743  mideulem  28744  midex  28745  oppperpex  28761  hpgid  28774  lnperpex  28811  trgcopy  28812  grpoidinv  30527  pjhthlem2  31411  mdsymlem3  32424  xrge0tsmsd  33065  isdrng4  33298  drngidl  33461  ssdifidlprm  33486  qsdrngi  33523  ballotlemfc0  34495  ballotlemfcc  34496  cvmliftlem15  35303  unblimceq0  36508  knoppndvlem18  36530  lhpexle3lem  40013  lhpex2leN  40015  cdlemg1cex  40590  fsuppind  42600  nacsfix  42723  unxpwdom3  43107  rfcnnnub  45041  climxrrelem  45764  climxrre  45765  xlimxrre  45846  stoweidlem27  46042  thinciso  49117
  Copyright terms: Public domain W3C validator