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

Theorem 2eximi 1910
 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 1909 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1909 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1851 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884 This theorem depends on definitions:  df-bi 197  df-ex 1852 This theorem is referenced by:  2mo  2687  2eu6  2694  cgsex2g  3377  cgsex4g  3378  vtocl2  3399  vtocl3  3400  dtru  5004  mosubopt  5118  elopaelxp  5346  ssrel  5362  relopabi  5399  xpdifid  5718  ssoprab2i  6912  hash1to3  13463  isfunc  16723  umgr3v3e3cycl  27334  frgrconngr  27446  bnj605  31282  bnj607  31291  bnj916  31308  bnj996  31330  bnj907  31340  bnj1128  31363  bj-dtru  33101  cnfinltrel  33550  ac6s6f  34292  2uasbanh  39277  2uasbanhVD  39644  elsprel  42233  sprssspr  42239
 Copyright terms: Public domain W3C validator