Theorem 19.41vv 1915

Description: Version of 19.41 2103 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)

Assertion

Ref	Expression
19.41vv	|- ( E. x E. y ( ph /\ ps ) <-> ( E. x E. y ph /\ ps ) )

Distinct variable groups:   ps, x   ps, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem 19.41vv

Step	Hyp	Ref	Expression
1		19.41v 1914	. . 3 |- ( E. y ( ph /\ ps ) <-> ( E. y ph /\ ps ) )
2	1	exbii 1774	. 2 |- ( E. x E. y ( ph /\ ps ) <-> E. x ( E. y ph /\ ps ) )
3		19.41v 1914	. 2 |- ( E. x ( E. y ph /\ ps ) <-> ( E. x E. y ph /\ ps ) )
4	2, 3	bitri 264	1 |- ( E. x E. y ( ph /\ ps ) <-> ( E. x E. y ph /\ 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.41vvv  1916  rabxp  5154  copsex2gb  5230  mpt2mptx  6751  xpassen  8054  dfac5lem1  8946  fusgr2wsp2nb  27198  bnj996  31025  dfdm5  31676  dfrn5  31677  elima4  31679  brtxp2  31988  brpprod3a  31993  brimg  32044  brsuccf  32048  diblsmopel  36460  mpt2mptx2  42113