Theorem 2exbidv 1845

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 1802	. 2 |- ( ph -> ( E. y ps <-> E. y ch ) )
3	2	exbidv 1802	1 |- ( ph -> ( E. x E. y ps <-> E. x E. y ch ) )

Syntax hints:   -> wi 4   <-> wb 104   E.wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-17 1503  ax-ial 1511

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbidv  1846  4exbidv  1847  cbvex4v  1907  ceqsex3v  2751  ceqsex4v  2752  copsexg  4199  euotd  4209  elopab  4213  elxpi  4595  relop  4729  cbvoprab3  5887  ov6g  5948  th3qlem1  6571  ltresr  7738  fisumcom2  11312  fprodcom2fi  11500