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

Theorem reximdvai 3161
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 3112 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rexim 3154 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
42, 3syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wral 3055  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061
This theorem is referenced by:  reximdv  3162  reximdva  3163  reuind  3572  wefrc  5271  isomin  6779  isofrlem  6782  onfununi  7642  oaordex  7843  odi  7864  omass  7865  omeulem1  7867  noinfep  8772  rankwflemb  8871  infxpenlem  9087  coflim  9336  coftr  9348  zorn2lem7  9577  suplem1pr  10127  axpre-sup  10243  climbdd  14687  filufint  22003  cvati  29681  atcvat4i  29712  mdsymlem2  29719  mdsymlem3  29720  sumdmdii  29730  iccllysconn  31680  dftrpred3g  32176  incsequz2  33967  lcvat  34986  hlrelat3  35368  cvrval3  35369  cvrval4N  35370  2atlt  35395  cvrat4  35399  atbtwnexOLDN  35403  atbtwnex  35404  athgt  35412  2llnmat  35480  lnjatN  35736  2lnat  35740  cdlemb  35750  lhpexle3lem  35967  cdlemf1  36517  cdlemf2  36518  cdlemf  36519  cdlemk26b-3  36861  dvh4dimlem  37399  upbdrech  40158  limcperiod  40498  cncfshift  40725  cncfperiod  40730
  Copyright terms: Public domain W3C validator