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

Theorem 2eximi 1803
 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 1802 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1802 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1744 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197  df-ex 1745 This theorem is referenced by:  2mo  2580  2eu6  2587  cgsex2g  3270  cgsex4g  3271  vtocl2  3292  vtocl3  3293  dtru  4887  mosubopt  5001  elopaelxp  5225  ssrel  5241  relopabi  5278  xpdifid  5597  ssoprab2i  6791  hash1to3  13311  isfunc  16571  umgr3v3e3cycl  27162  frgrconngr  27274  bnj605  31103  bnj607  31112  bnj916  31129  bnj996  31151  bnj907  31161  bnj1128  31184  bj-dtru  32922  ac6s6f  34111  2uasbanh  39094  2uasbanhVD  39461  elsprel  42050  sprssspr  42056
 Copyright terms: Public domain W3C validator