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

Theorem reximdvai 3154
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
Hypothesis
Ref Expression
reximdvai.1 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
Assertion
Ref Expression
reximdvai (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdvai
StepHypRef Expression
1 reximdvai.1 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
21imdistand 569 . 2 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
32reximdv2 3153 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2098  wrex 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060
This theorem is referenced by:  reximdva  3157  reximdv  3159  reuind  3745  wefrc  5672  isomin  7344  isofrlem  7347  onfununi  8362  oaordex  8579  odi  8600  omass  8601  omeulem1  8603  noinfep  9685  rankwflemb  9818  infxpenlem  10038  coflim  10286  coftr  10298  zorn2lem7  10527  suplem1pr  11077  axpre-sup  11194  climbdd  15654  filufint  23868  cvati  32248  atcvat4i  32279  mdsymlem2  32286  mdsymlem3  32287  sumdmdii  32297  iccllysconn  34991  incsequz2  37353  lcvat  38632  hlrelat3  39015  cvrval3  39016  cvrval4N  39017  2atlt  39042  cvrat4  39046  atbtwnexOLDN  39050  atbtwnex  39051  athgt  39059  2llnmat  39127  lnjatN  39383  2lnat  39387  cdlemb  39397  lhpexle3lem  39614  cdlemf1  40164  cdlemf2  40165  cdlemf  40166  cdlemk26b-3  40508  dvh4dimlem  41046  cantnf2  42896  upbdrech  44825  limcperiod  45154  cncfshift  45400  cncfperiod  45405
  Copyright terms: Public domain W3C validator