Theorem 19.42vv 1898

Description: Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)

Assertion

Ref	Expression
19.42vv	|- ( E. x E. y ( ph /\ ps ) <-> ( ph /\ E. x E. y ps ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)

Proof of Theorem 19.42vv

Step	Hyp	Ref	Expression
1		exdistr 1896	. 2 |- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
2		19.42v 1893	. 2 |- ( E. x ( ph /\ E. y ps ) <-> ( ph /\ E. x E. y ps ) )
3	1, 2	bitri 183	1 |- ( E. x E. y ( ph /\ ps ) <-> ( ph /\ E. x E. y ps ) )

Syntax hints:   /\ wa 103   <-> wb 104   E.wex 1479

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.42vvv  1899  19.42vvvv  1900  exdistr2  1901  3exdistr  1902  ceqsex3v  2763  ceqsex4v  2764  elvvv  4661  dfoprab2  5880  resoprab  5929  ovi3  5969  ov6g  5970  oprabex3  6089  xpassen  6787  enq0enq  7363  enq0sym  7364  nqnq0pi  7370  axaddf  7800  axmulf  7801