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

Theorem 2eximi 1830
Description: Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
eximi.1 (𝜑𝜓)
Assertion
Ref Expression
2eximi (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)

Proof of Theorem 2eximi
StepHypRef Expression
1 eximi.1 . . 3 (𝜑𝜓)
21eximi 1829 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1829 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-ex 1774
This theorem is referenced by:  2mo  2636  2eu6  2645  cgsex2g  3508  cgsex4g  3509  cgsex4gOLD  3510  cgsex4gOLDOLD  3511  dtruALT2  5370  exexneq  5436  dtruOLD  5443  mosubopt  5512  elopaelxpOLD  5768  ssrel  5784  ssrelOLD  5785  relopabi  5824  xpdifid  6174  ssoprab2i  7531  hash1to3  14496  catcone0  17686  isfunc  17869  umgr3v3e3cycl  30086  frgrconngr  30196  bnj605  34689  bnj607  34698  bnj916  34715  bnj996  34738  bnj907  34749  bnj1128  34772  funen1cnv  34862  cusgr3cyclex  34897  acycgrislfgr  34913  umgracycusgr  34915  cusgracyclt3v  34917  ac6s6f  37797  mnringmulrcld  43812  2uasbanh  44147  2uasbanhVD  44497  elsprel  46957  sprssspr  46963  2exopprim  47007  reuopreuprim  47008
  Copyright terms: Public domain W3C validator