Theorem ralbid 2891

Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.)

Hypotheses

Ref	Expression
ralbid.1
ralbid.2

Assertion

Ref	Expression
ralbid

Proof of Theorem ralbid

Step	Hyp	Ref	Expression
1		ralbid.1	. 2
2		ralbid.2	. . 3
3	2	adantr 465	. 2
4	1, 3	ralbida 2890	1

Syntax hints:  ->wi 4  <->wb 184  F/wnf 1616  e.wcel 1818  A.wral 2807

This theorem is referenced by:  ralbidvOLD  2897  raleqbid  3066  sbcralt  3408  sbcrextOLD  3409  sbcrext  3410  riota5f  6282  zfrep6  6768  cnfcom3clem  8170  cnfcom3clemOLD  8178  cplem2  8329  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  acnlem  8450  lble  10520  fsuppmapnn0fiubex  12098  chirred  27314  indexa  30224  climf  31628  cncficcgt0  31691  stoweidlem16  31798  stoweidlem18  31800  stoweidlem21  31803  stoweidlem29  31811  stoweidlem31  31813  stoweidlem36  31818  stoweidlem41  31823  stoweidlem44  31826  stoweidlem45  31827  stoweidlem51  31833  stoweidlem55  31837  stoweidlem59  31841  stoweidlem60  31842  riotasvd  34687  cdlemk36  36639

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-ral 2812