ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralbidva Structured version   GIF version

Theorem ralbidva 2316
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1 ((φ x A) → (ψχ))
Assertion
Ref Expression
ralbidva (φ → (x A ψx A χ))
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   χ(x)   A(x)

Proof of Theorem ralbidva
StepHypRef Expression
1 nfv 1418 . 2 xφ
2 ralbidva.1 . 2 ((φ x A) → (ψχ))
31, 2ralbida 2314 1 (φ → (x A ψx A χ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   wcel 1390  wral 2300
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305
This theorem is referenced by:  raleqbidva  2513  poinxp  4352  funimass4  5167  funimass3  5226  funconstss  5228  cocan1  5370  cocan2  5371  isocnv2  5395  isores2  5396  isoini2  5401  ofrfval  5662  ofrfval2  5669  dfsmo2  5843  smores  5848  smores2  5850  zextlt  8088  prime  8093  fzshftral  8720
  Copyright terms: Public domain W3C validator