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

Theorem 3exbii 1571
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 1569 . 2  |-  ( E. z ph  <->  E. z ps )
322exbii 1570 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 1528
This theorem is referenced by:  eeeanv  1855  ceqsex6v  2828  oprabid  5882  dfoprab2  5895  dftpos3  6252  xpassen  6956  ellines  24775  eeeeanv  24944  isalg  25721  algi  25727  bnj916  28965  bnj917  28966  bnj983  28983  bnj996  28987  bnj1021  28996  bnj1033  28999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator