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

Theorem 2eximi 1753
 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 1752 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1752 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  2mo  2539  2eu6  2546  cgsex2g  3212  cgsex4g  3213  vtocl2  3234  vtocl3  3235  dtru  4783  mosubopt  4897  elopaelxp  5114  ssrel  5130  relopabi  5167  xpdifid  5481  ssoprab2i  6647  hash1to3  13128  isfunc  16347  usgraop  25879  usgraedg4  25916  3v3e3cycl2  26192  frconngra  26548  bnj605  30231  bnj607  30240  bnj916  30257  bnj996  30279  bnj907  30289  bnj1128  30312  bj-dtru  31985  ac6s6f  33151  2uasbanh  37798  2uasbanhVD  38169  umgr3v3e3cycl  41351  frgrconngr  41464
 Copyright terms: Public domain W3C validator