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

Theorem 2eximi 1836
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 1835 . 2 (∃𝑦𝜑 → ∃𝑦𝜓)
32eximi 1835 1 (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  2mo  2648  2eu6  2657  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  dtruALT2  5370  exexneq  5439  dtruOLD  5446  mosubopt  5515  elopaelxpOLD  5776  ssrel  5792  ssrelOLD  5793  relopabi  5832  xpdifid  6188  ssoprab2i  7544  hash1to3  14531  catcone0  17730  isfunc  17909  umgr3v3e3cycl  30203  frgrconngr  30313  bnj605  34921  bnj607  34930  bnj916  34947  bnj996  34970  bnj907  34981  bnj1128  35004  funen1cnv  35102  cusgr3cyclex  35141  acycgrislfgr  35157  umgracycusgr  35159  cusgracyclt3v  35161  ac6s6f  38180  mnringmulrcld  44247  2uasbanh  44581  2uasbanhVD  44931  elsprel  47462  sprssspr  47468  2exopprim  47512  reuopreuprim  47513
  Copyright terms: Public domain W3C validator