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

Theorem 2eximi 1708
Description: Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
eximi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
2eximi  |-  ( E. x E. y ph  ->  E. x E. y ps )

Proof of Theorem 2eximi
StepHypRef Expression
1 eximi.1 . . 3  |-  ( ph  ->  ps )
21eximi 1707 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1707 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-ex 1664
This theorem is referenced by:  2mo  2380  2eu6  2387  cgsex2g  3081  cgsex4g  3082  vtocl2  3102  vtocl3  3103  dtru  4594  mosubopt  4699  elopaelxp  4907  xpdifid  5265  ssoprab2i  6385  hash1to3  12648  isfunc  15769  usgraop  25077  usgraedg4  25114  3v3e3cycl2  25392  frconngra  25749  bnj605  29718  bnj607  29727  bnj916  29744  bnj996  29766  bnj907  29776  bnj1128  29799  bj-dtru  31412  ac6s6f  32416  2uasbanh  36928  2uasbanhVD  37308
  Copyright terms: Public domain W3C validator