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

Theorem ralbidv 2320
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 1418 . 2 xφ
2 ralbidv.1 . 2 (φ → (ψχ))
31, 2ralbid 2318 1 (φ → (x A ψx A χ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  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:  ralbii  2324  2ralbidv  2342  rexralbidv  2344  r19.32vdc  2453  raleqbi1dv  2507  raleqbidv  2511  cbvral2v  2535  rspc2  2655  rspc3v  2659  reu6i  2726  reu7  2730  sbcralt  2828  sbcralg  2830  raaanlem  3320  r19.12sn  3427  2ralunsn  3560  elintg  3614  elintrabg  3619  eliin  3653  bnd2  3917  poeq1  4027  soeq1  4043  reusv3  4158  posng  4355  ralxpf  4425  cnvpom  4803  funcnvuni  4911  dff4im  5256  dff13f  5352  eusvobj2  5441  ofreq  5657  smoeq  5846  recseq  5862  tfr0  5878  tfrlemiex  5886  elinp  6456  prloc  6473  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  nnsub  7713  indstr  8292  ublbneg  8304  lbzbi  8307  iccsupr  8585  bj-omtrans  9390
  Copyright terms: Public domain W3C validator