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

Theorem 3exbii 1574
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 1572 . 2  |-  ( E. z ph  <->  E. z ps )
322exbii 1573 1  |-  ( E. x E. y E. z ph  <->  E. x E. y E. z ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1531
This theorem is referenced by:  eeeanv  1867  ceqsex6v  2841  oprabid  5898  dfoprab2  5911  dftpos3  6268  xpassen  6972  ellines  24847  eeeeanv  25047  isalg  25824  algi  25830  bnj916  29281  bnj917  29282  bnj983  29299  bnj996  29303  bnj1021  29312  bnj1033  29315  eeeanvOLD7  29658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator