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

Theorem reximddv 3165
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 458 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
43reximdva 3162 . 2 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
51, 4mpd 15 1 (𝜑 → ∃𝑥𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3071
This theorem is referenced by:  reximddv2  3203  dedekind  11323  caucvgrlem  15563  isprm5  16588  drsdirfi  18199  sylow2  19413  gexex  19636  nrmsep  22724  regsep2  22743  locfincmp  22893  dissnref  22895  met1stc  23893  xrge0tsms  24213  cnheibor  24334  lmcau  24693  ismbf3d  25034  ulmdvlem3  25777  legov  27569  legtrid  27575  midexlem  27676  opphllem  27719  mideulem  27720  midex  27721  oppperpex  27737  hpgid  27750  lnperpex  27787  trgcopy  27788  grpoidinv  29492  pjhthlem2  30376  mdsymlem3  31389  xrge0tsmsd  31948  ballotlemfc0  33149  ballotlemfcc  33150  cvmliftlem15  33949  unblimceq0  35016  knoppndvlem18  35038  lhpexle3lem  38520  lhpex2leN  38522  cdlemg1cex  39097  fsuppind  40808  nacsfix  41078  unxpwdom3  41465  rfcnnnub  43329  reximddv3  43449  climxrrelem  44076  climxrre  44077  xlimxrre  44158  stoweidlem27  44354  thinciso  47166
  Copyright terms: Public domain W3C validator