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

Theorem reximdvai 3151
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.)
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 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
21ralrimiv 3101 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rexim 3144 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
42, 3syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2137  wral 3048  wrex 3049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1852  df-ral 3053  df-rex 3054
This theorem is referenced by:  reximdv  3152  reximdva  3153  reuind  3550  wefrc  5258  isomin  6748  isofrlem  6751  onfununi  7605  oaordex  7805  odi  7826  omass  7827  omeulem1  7829  noinfep  8728  rankwflemb  8827  infxpenlem  9024  coflim  9273  coftr  9285  zorn2lem7  9514  suplem1pr  10064  axpre-sup  10180  climbdd  14599  filufint  21923  cvati  29532  atcvat4i  29563  mdsymlem2  29570  mdsymlem3  29571  sumdmdii  29581  iccllysconn  31537  dftrpred3g  32036  incsequz2  33856  lcvat  34818  hlrelat3  35199  cvrval3  35200  cvrval4N  35201  2atlt  35226  cvrat4  35230  atbtwnexOLDN  35234  atbtwnex  35235  athgt  35243  2llnmat  35311  lnjatN  35567  2lnat  35571  cdlemb  35581  lhpexle3lem  35798  cdlemf1  36349  cdlemf2  36350  cdlemf  36351  cdlemk26b-3  36693  dvh4dimlem  37232  upbdrech  40016  limcperiod  40361  cncfshift  40588  cncfperiod  40593
  Copyright terms: Public domain W3C validator