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

Theorem 2eximi 1827
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 1826 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1826 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  2mo  2726  2eu6  2737  cgsex2g  3536  cgsex4g  3537  vtocl2OLD  3560  dtru  5262  mosubopt  5391  elopaelxp  5634  ssrel  5650  relopabi  5687  xpdifid  6018  ssoprab2i  7252  hash1to3  13837  isfunc  17122  umgr3v3e3cycl  27890  frgrconngr  28000  bnj605  32078  bnj607  32087  bnj916  32104  bnj996  32126  bnj907  32136  bnj1128  32159  funen1cnv  32254  cusgr3cyclex  32280  acycgrislfgr  32296  umgracycusgr  32298  cusgracyclt3v  32300  bj-dtru  34036  ac6s6f  35332  sn-dtru  38989  2uasbanh  40772  2uasbanhVD  41122  elsprel  43514  sprssspr  43520  2exopprim  43564  reuopreuprim  43565
  Copyright terms: Public domain W3C validator