Theorem 19.42vv 1920

Description: Version of 19.42 2105 with two quantifiers and a dv condition requiring fewer axioms. (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 1919	. 2 |- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
2		19.42v 1918	. 2 |- ( E. x ( ph /\ E. y ps ) <-> ( ph /\ E. x E. y ps ) )
3	1, 2	bitri 264	1 |- ( E. x E. y ( ph /\ ps ) <-> ( ph /\ E. x E. y ps ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  19.42vvv  1921  exdistr2  1922  3exdistr  1923  ceqsex3v  3246  ceqsex4v  3247  ceqsex8v  3249  elvvv  5178  xpdifid  5562  dfoprab2  6701  resoprab  6756  elrnmpt2res  6774  ov3  6797  ov6g  6798  oprabex3  7157  xpassen  8054  axaddf  9966  axmulf  9967  qqhval2  30026  bnj996  31025  dvhopellsm  36406