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

Step	Hyp	Ref	Expression
1		3exbii.1	. . 3
2	1	exbii 1667	. 2
3	2	2exbii 1668	1

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