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

Theorem 2eximi 1760
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 1759 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1759 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  2mo  2550  2eu6  2557  cgsex2g  3229  cgsex4g  3230  vtocl2  3251  vtocl3  3252  dtru  4827  mosubopt  4942  elopaelxp  5162  ssrel  5178  relopabi  5215  xpdifid  5531  ssoprab2i  6714  hash1to3  13228  isfunc  16464  umgr3v3e3cycl  26944  frgrconngr  27056  bnj605  30738  bnj607  30747  bnj916  30764  bnj996  30786  bnj907  30796  bnj1128  30819  bj-dtru  32493  ac6s6f  33652  2uasbanh  38298  2uasbanhVD  38669  elsprel  41043  sprssspr  41049
  Copyright terms: Public domain W3C validator