Theorem 2rexbidv 2489

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

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

Distinct variable groups:   ph, x   ph, y

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

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	rexbidv 2465	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2465	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 104   E.wrex 2443

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-rex 2448

This theorem is referenced by:  f1oiso  5788  elrnmpog  5945  elrnmpo  5946  ralrnmpo  5947  rexrnmpo  5948  ovelrn  5981  eroveu  6583  genipv  7441  genpelxp  7443  genpelvl  7444  genpelvu  7445  axcnre  7813  apreap  8476  apreim  8492  aprcl  8535  bezoutlemnewy  11914  bezoutlema  11917  bezoutlemb  11918  pythagtriplem19  12191  pceu  12204  pcval  12205  pczpre  12206  pcdiv  12211  txuni2  12797  txbas  12799  txdis1cn  12819