Theorem 2ralbidva 2706

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)

Hypothesis

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

Assertion

Ref	Expression
2ralbidva	|- ( ph -> ( A. x e. A A. y e. B ps <-> A. x e. A A. 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 2ralbidva

Step	Hyp	Ref	Expression
1		nfv 1626	. 2 |- F/ x ph
2		nfv 1626	. 2 |- F/ y ph
3		2ralbidva.1	. 2 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps <-> ch ) )
4	1, 2, 3	2ralbida 2705	1 |- ( ph -> ( A. x e. A A. y e. B ps <-> A. x e. A A. y e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   e. wcel 1721   A.wral 2666

This theorem is referenced by:  disjxun  4170  isocnv3  6011  isotr  6015  f1oweALT  6033  tosso  14420  pospropd  14516  isipodrs  14542  mndpropd  14676  mhmpropd  14699  efgred  15335  cmnpropd  15376  rngpropd  15650  lmodprop2d  15961  lsspropd  16048  islmhm2  16069  lmhmpropd  16100  assapropd  16341  connsub  17437  hausdiag  17630  ist0-4  17714  ismet2  18316  txmetcnp  18530  txmetcn  18531  metuel2  18562  metucnOLD  18571  metucn  18572  isngp3  18598  nlmvscn  18676  ipcn  19153  iscfil2  19172  caucfil  19189  cfilresi  19201  ulmdvlem3  20271  cxpcn3  20585  isarchi2  24208  ghomgsg  25057  brbtwn2  25748  colinearalglem2  25750  isbnd3b  26384  gicabl  27131  islindf4  27176  isdomn3  27391  iscvlat2N  29807  ishlat3N  29837

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671