MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3exbii Structured version   Unicode version

Theorem 3exbii 1595
Description: Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
Hypothesis
Ref Expression
3exbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
3exbii  |-  ( E. x E. y E. z ph  <->  E. x E. y E. z ps )

Proof of Theorem 3exbii
StepHypRef Expression
1 3exbii.1 . . 3  |-  ( ph  <->  ps )
21exbii 1593 . 2  |-  ( E. z ph  <->  E. z ps )
322exbii 1594 1  |-  ( E. x E. y E. z ph  <->  E. x E. y E. z ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1551
This theorem is referenced by:  4exdistr  1935  eeeanvOLD  1940  ceqsex6v  2997  oprabid  6106  dfoprab2  6122  dftpos3  6498  xpassen  7203  ellines  26087  bnj916  29305  bnj917  29306  bnj983  29323  bnj996  29327  bnj1021  29336  bnj1033  29339  eeeanvOLD7  29705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator