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

Theorem 2eximi 1798
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 1797 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1797 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772
This theorem depends on definitions:  df-bi 199  df-ex 1743
This theorem is referenced by:  2mo  2679  2eu6  2688  cgsex2g  3459  cgsex4g  3460  vtocl2OLD  3481  dtru  5125  mosubopt  5257  elopaelxp  5492  ssrel  5508  relopabi  5545  xpdifid  5867  ssoprab2i  7081  hash1to3  13663  isfunc  16995  umgr3v3e3cycl  27716  frgrconngr  27831  bnj605  31826  bnj607  31835  bnj916  31852  bnj996  31874  bnj907  31884  bnj1128  31907  bj-dtru  33625  ac6s6f  34895  sn-dtru  38556  2uasbanh  40314  2uasbanhVD  40664  elsprel  43006  sprssspr  43012  2exopprim  43056  reuopreuprim  43057
  Copyright terms: Public domain W3C validator