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

Theorem 2eximi 1837
 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 1836 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1836 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ex 1782 This theorem is referenced by:  2mo  2736  2eu6  2745  cgsex2g  3524  cgsex4g  3525  vtocl2OLD  3548  dtru  5258  mosubopt  5387  elopaelxp  5628  ssrel  5644  relopabi  5681  xpdifid  6012  ssoprab2i  7256  hash1to3  13854  isfunc  17134  umgr3v3e3cycl  27976  frgrconngr  28086  bnj605  32240  bnj607  32249  bnj916  32266  bnj996  32289  bnj907  32300  bnj1128  32323  funen1cnv  32418  cusgr3cyclex  32444  acycgrislfgr  32460  umgracycusgr  32462  cusgracyclt3v  32464  bj-dtru  34202  ac6s6f  35560  sn-dtru  39343  mnringmulrcld  40861  2uasbanh  41192  2uasbanhVD  41542  elsprel  43923  sprssspr  43929  2exopprim  43973  reuopreuprim  43974
 Copyright terms: Public domain W3C validator