Theorem 2rexbidv 2515

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 2491	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2491	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 105   E.wrex 2469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-rex 2474

This theorem is referenced by:  f1oiso  5848  elrnmpog  6010  elrnmpo  6011  ralrnmpo  6012  rexrnmpo  6013  ovelrn  6046  eroveu  6653  genipv  7539  genpelxp  7541  genpelvl  7542  genpelvu  7543  axcnre  7911  apreap  8575  apreim  8591  aprcl  8634  aptap  8638  bezoutlemnewy  12032  bezoutlema  12035  bezoutlemb  12036  pythagtriplem19  12317  pceu  12330  pcval  12331  pczpre  12332  pcdiv  12337  4sqlem2  12424  4sqlem3  12425  4sqlem4  12427  4sqexercise2  12434  4sqlemsdc  12435  4sq  12445  txuni2  14233  txbas  14235  txdis1cn  14255  2sqlem2  14940  2sqlem8  14948  2sqlem9  14949