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

Theorem 2eximi 1752
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 1751 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1751 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  2mo  2538  2eu6  2545  cgsex2g  3211  cgsex4g  3212  vtocl2  3233  vtocl3  3234  dtru  4778  mosubopt  4888  elopaelxp  5104  xpdifid  5467  ssoprab2i  6625  hash1to3  13078  isfunc  16293  usgraop  25645  usgraedg4  25682  3v3e3cycl2  25958  frconngra  26314  bnj605  30037  bnj607  30046  bnj916  30063  bnj996  30085  bnj907  30095  bnj1128  30118  bj-dtru  31791  ac6s6f  32947  2uasbanh  37594  2uasbanhVD  37965  umgr3v3e3cycl  41346  frgrconngr  41459
  Copyright terms: Public domain W3C validator