Theorem 19.42vv 1935

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 1933	. 2 |- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
2		19.42v 1930	. 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 1515

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.42vvv  1936  19.42vvvv  1937  exdistr2  1938  3exdistr  1939  ceqsex3v  2815  ceqsex4v  2816  elvvv  4739  dfoprab2  5994  resoprab  6043  ovi3  6085  ov6g  6086  oprabex3  6216  xpassen  6927  enq0enq  7546  enq0sym  7547  nqnq0pi  7553  axaddf  7983  axmulf  7984