Theorem 2exbidv 1868

Description: Formula-building rule for 2 existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)

Hypothesis

Ref	Expression
2albidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
2exbidv	|- ( ph -> ( E. x E. y ps <-> E. x E. y ch ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)   ch( x, y)

Proof of Theorem 2exbidv

Step	Hyp	Ref	Expression
1		2albidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	exbidv 1825	. 2 |- ( ph -> ( E. y ps <-> E. y ch ) )
3	2	exbidv 1825	1 |- ( ph -> ( E. x E. y ps <-> E. x E. y ch ) )

Syntax hints:   -> wi 4   <-> wb 105   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbidv  1869  4exbidv  1870  cbvex4v  1930  ceqsex3v  2781  ceqsex4v  2782  copsexg  4246  euotd  4256  elopab  4260  elxpi  4644  relop  4779  cbvoprab3  5954  ov6g  6015  th3qlem1  6640  ltresr  7841  fisumcom2  11449  fprodcom2fi  11637