Theorem 19.42vv 1936

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 1934	. 2 |- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
2		19.42v 1931	. 2 |- ( E. x ( ph /\ E. y ps ) <-> ( ph /\ E. x E. y ps ) )
3	1, 2	bitri 184	1 |- ( E. x E. y ( ph /\ ps ) <-> ( ph /\ E. x E. y ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   E.wex 1516

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.42vvv  1937  19.42vvvv  1938  exdistr2  1939  3exdistr  1940  ceqsex3v  2820  ceqsex4v  2821  elvvv  4756  dfoprab2  6015  resoprab  6064  ovi3  6106  ov6g  6107  oprabex3  6237  xpassen  6950  enq0enq  7579  enq0sym  7580  nqnq0pi  7586  axaddf  8016  axmulf  8017