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

Theorem reximdvai 3232
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 3146 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rexim 3203 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
42, 3syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2079  wral 3103  wrex 3104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-ral 3108  df-rex 3109
This theorem is referenced by:  reximdv  3233  reximdva  3234  reuind  3673  wefrc  5429  isomin  6944  isofrlem  6947  onfununi  7821  oaordex  8025  odi  8046  omass  8047  omeulem1  8049  noinfep  8958  rankwflemb  9057  infxpenlem  9274  coflim  9518  coftr  9530  zorn2lem7  9759  suplem1pr  10309  axpre-sup  10426  climbdd  14850  filufint  22200  cvati  29822  atcvat4i  29853  mdsymlem2  29860  mdsymlem3  29861  sumdmdii  29871  iccllysconn  32061  dftrpred3g  32626  incsequz2  34502  lcvat  35647  hlrelat3  36029  cvrval3  36030  cvrval4N  36031  2atlt  36056  cvrat4  36060  atbtwnexOLDN  36064  atbtwnex  36065  athgt  36073  2llnmat  36141  lnjatN  36397  2lnat  36401  cdlemb  36411  lhpexle3lem  36628  cdlemf1  37178  cdlemf2  37179  cdlemf  37180  cdlemk26b-3  37522  dvh4dimlem  38060  upbdrech  41066  limcperiod  41405  cncfshift  41652  cncfperiod  41657
  Copyright terms: Public domain W3C validator