Theorem 2rexbidva 3056

Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)

Hypothesis

Ref	Expression
2rexbidva.1	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps <-> ch ) )

Assertion

Ref	Expression
2rexbidva	|- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )

Distinct variable groups:   x, y, ph   y, A

Allowed substitution hints:   ps( x, y)   ch( x, y)   A( x)   B( x, y)

Proof of Theorem 2rexbidva

Step	Hyp	Ref	Expression
1		2rexbidva.1	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps <-> ch ) )
2	1	anassrs 680	. . 3 |- ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ps <-> ch ) )
3	2	rexbidva 3049	. 2 |- ( ( ph /\ x e. A ) -> ( E. y e. B ps <-> E. y e. B ch ) )
4	3	rexbidva 3049	1 |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   e. wcel 1990   E.wrex 2913

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

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

This theorem is referenced by:  wrdl3s3  13705  bezoutlem2  15257  bezoutlem4  15259  vdwmc2  15683  lsmcom2  18070  lsmass  18083  lsmcomx  18259  lsmspsn  19084  hausdiag  21448  imasf1oxms  22294  istrkg2ld  25359  iscgra  25701  axeuclid  25843  wwlksnwwlksnon  26810  wspthsnwspthsnon  26811  elwwlks2  26861  elwspths2spth  26862  fusgr2wsp2nb  27198  shscom  28178  3dim0  34743  islpln5  34821  islvol5  34865  isline2  35060  isline3  35062  paddcom  35099  cdlemg2cex  35879  2reu4a  41189  pgrpgt2nabl  42147  elbigolo1  42351