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

Theorem 3exbii 1669
Description: Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
Hypothesis
Ref Expression
3exbii.1
Assertion
Ref Expression
3exbii

Proof of Theorem 3exbii
StepHypRef Expression
1 3exbii.1 . . 3
21exbii 1667 . 2
322exbii 1668 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  E.wex 1612
This theorem is referenced by:  4exdistr  1781  ceqsex6v  3151  oprabid  6323  dfoprab2  6343  dftpos3  6992  xpassen  7631  ellines  29802  bnj916  33991  bnj917  33992  bnj983  34009  bnj996  34013  bnj1021  34022  bnj1033  34025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator