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

Theorem reximdvai 3165
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 570 . 2 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐴𝜒)))
32reximdv2 3164 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  reximdva  3168  reximdv  3170  reuind  3759  wefrc  5679  isomin  7357  isofrlem  7360  onfununi  8381  oaordex  8596  odi  8617  omass  8618  omeulem1  8620  noinfep  9700  rankwflemb  9833  infxpenlem  10053  coflim  10301  coftr  10313  zorn2lem7  10542  suplem1pr  11092  axpre-sup  11209  climbdd  15708  filufint  23928  cvati  32385  atcvat4i  32416  mdsymlem2  32423  mdsymlem3  32424  sumdmdii  32434  iccllysconn  35255  incsequz2  37756  lcvat  39031  hlrelat3  39414  cvrval3  39415  cvrval4N  39416  2atlt  39441  cvrat4  39445  atbtwnexOLDN  39449  atbtwnex  39450  athgt  39458  2llnmat  39526  lnjatN  39782  2lnat  39786  cdlemb  39796  lhpexle3lem  40013  cdlemf1  40563  cdlemf2  40564  cdlemf  40565  cdlemk26b-3  40907  dvh4dimlem  41445  cantnf2  43338  relpfrlem  44974  upbdrech  45317  limcperiod  45643  cncfshift  45889  cncfperiod  45894
  Copyright terms: Public domain W3C validator