Theorem 2ralbidva 2841

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.)

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		2ralbidva.1	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps <-> ch ) )
2	1	anassrs 658	. . 3 |- ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ps <-> ch ) )
3	2	ralbidva 2835	. 2 |- ( ( ph /\ x e. A ) -> ( A. y e. B ps <-> A. y e. B ch ) )
4	3	ralbidva 2835	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 189   /\ wa 375   e. wcel 1897   A.wral 2748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768

This theorem depends on definitions:  df-bi 190  df-an 377  df-ral 2753

This theorem is referenced by:  disjxun  4413  isocnv3  6247  isotr  6251  f1oweALT  6803  fnmpt2ovd  6897  tosso  16330  pospropd  16428  isipodrs  16455  mndpropd  16610  mhmpropd  16636  efgred  17446  cmnpropd  17487  ringpropd  17860  lmodprop2d  18198  lsspropd  18288  islmhm2  18309  lmhmpropd  18344  assapropd  18599  islindf4  19444  scmatmats  19584  cpmatel2  19785  1elcpmat  19787  m2cpminvid2  19827  decpmataa0  19840  pmatcollpw2lem  19849  connsub  20484  hausdiag  20708  ist0-4  20792  ismet2  21396  txmetcnp  21610  txmetcn  21611  metuel2  21628  metucn  21634  isngp3  21660  nlmvscn  21738  ipcn  22265  iscfil2  22284  caucfil  22301  cfilresi  22313  ulmdvlem3  23405  cxpcn3  23736  tgcgr4  24624  perpcom  24806  brbtwn2  24983  colinearalglem2  24985  eengtrkg  25063  isarchi2  28550  elmrsubrn  30206  ghomgsg  30359  isbnd3b  32161  iscvlat2N  32934  ishlat3N  32964  gicabl  36001  isdomn3  36125  mgmpropd  40047  mgmhmpropd  40057  lidlmmgm  40197  lindslinindsimp2  40528