New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ralbidv GIF version

Theorem ralbidv 2634
 Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1 (φ → (ψχ))
Assertion
Ref Expression
ralbidv (φ → (x A ψx A χ))
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   χ(x)   A(x)

Proof of Theorem ralbidv
StepHypRef Expression
1 nfv 1619 . 2 xφ
2 ralbidv.1 . 2 (φ → (ψχ))
31, 2ralbid 2632 1 (φ → (x A ψx A χ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176  ∀wral 2614 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619 This theorem is referenced by:  ralbii  2638  2ralbidv  2656  rexralbidv  2658  raleqbi1dv  2815  raleqbidv  2819  cbvral2v  2843  rspc2  2960  rspc3v  2964  reu6i  3027  reu7  3031  sbcralt  3118  sbcralg  3120  raaan  3657  raaanv  3658  r19.12sn  3789  2ralunsn  3880  elintg  3934  elintrabg  3939  eliin  3974  nndisjeq  4429  evenodddisjlem1  4515  evenodddisj  4516  nnpweq  4523  ralxpf  4827  funcnvuni  5161  dff4  5421  dff13f  5472  trd  5921  extd  5923  trrd  5925  refrd  5926  refd  5927  nclenn  6249  nnc3n3p1  6278  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  nchoicelem19  6307
 Copyright terms: Public domain W3C validator