Theorem 2ralbidva 2896

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 646	. . 3 |- ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ps <-> ch ) )
3	2	ralbidva 2890	. 2 |- ( ( ph /\ x e. A ) -> ( A. y e. B ps <-> A. y e. B ch ) )
4	3	ralbidva 2890	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 184   /\ wa 367   e. wcel 1823   A.wral 2804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709

This theorem depends on definitions:  df-bi 185  df-an 369  df-ral 2809

This theorem is referenced by:  disjxun  4437  isocnv3  6203  isotr  6207  f1oweALT  6757  fnmpt2ovd  6851  tosso  15868  pospropd  15966  isipodrs  15993  mndpropd  16148  mhmpropd  16174  efgred  16968  cmnpropd  17009  ringpropd  17428  lmodprop2d  17770  lsspropd  17861  islmhm2  17882  lmhmpropd  17917  assapropd  18174  islindf4  19043  scmatmats  19183  cpmatel2  19384  1elcpmat  19386  m2cpminvid2  19426  decpmataa0  19439  pmatcollpw2lem  19448  connsub  20091  hausdiag  20315  ist0-4  20399  ismet2  21005  txmetcnp  21219  txmetcn  21220  metuel2  21251  metucnOLD  21260  metucn  21261  isngp3  21287  nlmvscn  21365  ipcn  21855  iscfil2  21874  caucfil  21891  cfilresi  21903  ulmdvlem3  22966  cxpcn3  23293  perpcom  24294  brbtwn2  24413  colinearalglem2  24415  eengtrkg  24493  isarchi2  27966  elmrsubrn  29147  ghomgsg  29300  isbnd3b  30524  gicabl  31291  isdomn3  31408  mgmpropd  32854  mgmhmpropd  32864  lidlmmgm  33004  lindslinindsimp2  33337  iscvlat2N  35465  ishlat3N  35495