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

Theorem reximdvai 3010
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 2960 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rexim 3003 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
42, 3syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wral 2907  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2912  df-rex 2913
This theorem is referenced by:  reximdv  3011  reximdva  3012  reuind  3397  wefrc  5073  isomin  6547  isofrlem  6550  onfununi  7390  oaordex  7590  odi  7611  omass  7612  omeulem1  7614  noinfep  8508  rankwflemb  8607  infxpenlem  8787  coflim  9034  coftr  9046  zorn2lem7  9275  suplem1pr  9825  axpre-sup  9941  climbdd  14343  filufint  21643  cvati  29092  atcvat4i  29123  mdsymlem2  29130  mdsymlem3  29131  sumdmdii  29141  iccllysconn  30967  dftrpred3g  31461  incsequz2  33204  lcvat  33824  hlrelat3  34205  cvrval3  34206  cvrval4N  34207  2atlt  34232  cvrat4  34236  atbtwnexOLDN  34240  atbtwnex  34241  athgt  34249  2llnmat  34317  lnjatN  34573  2lnat  34577  cdlemb  34587  lhpexle3lem  34804  cdlemf1  35356  cdlemf2  35357  cdlemf  35358  cdlemk26b-3  35700  dvh4dimlem  36239  upbdrech  39006  limcperiod  39287  cncfshift  39413  cncfperiod  39418
  Copyright terms: Public domain W3C validator