Theorem 19.42vv 1883

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 1881	. 2 |- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
2		19.42v 1878	. 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 1468

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.42vvv  1884  19.42vvvv  1885  exdistr2  1886  3exdistr  1887  ceqsex3v  2723  ceqsex4v  2724  elvvv  4597  dfoprab2  5811  resoprab  5860  ovi3  5900  ov6g  5901  oprabex3  6020  xpassen  6717  enq0enq  7232  enq0sym  7233  nqnq0pi  7239  axaddf  7669  axmulf  7670