Theorem r19.26-2 2985

Description: Restricted quantifier version of 19.26-2 1681. Version of r19.26 2984 with two quantifiers. (Contributed by NM, 10-Aug-2004.)

Assertion

Ref	Expression
r19.26-2

Proof of Theorem r19.26-2

Step	Hyp	Ref	Expression
1		r19.26 2984	. . 3
2	1	ralbii 2888	. 2
3		r19.26 2984	. 2
4	2, 3	bitri 249	1

Syntax hints:  <->wb 184  /\wa 369  A.wral 2807

This theorem is referenced by:  fununi  5659  tz7.48lem  7125  isffth2  15285  ispos2  15577  issgrpv  15913  issgrpn0  15914  isnsg2  16231  efgred  16766  dfrhm2  17366  cpmatacl  19217  cpmatmcllem  19219  caucfil  21722  aalioulem6  22733  ajmoi  25774  adjmo  26751  iccllyscon  28695  dfso3  29097  ispridl2  30435  isrnghm  32698  ishlat2  35078  fiinfi  37758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812