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  4738  dfoprab2  5992  resoprab  6041  ovi3  6083  ov6g  6084  oprabex3  6214  xpassen  6925  enq0enq  7544  enq0sym  7545  nqnq0pi  7551  axaddf  7981  axmulf  7982