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  3426  2ralunsn  3559  elintg  3613  elintrabg  3618  eliin  3652  bnd2  3916  poeq1  4026  soeq1  4042  reusv3  4157  posng  4354  ralxpf  4424  cnvpom  4802  funcnvuni  4909  dff4im  5254  dff13f  5350  eusvobj2  5438  ofreq  5654  smoeq  5843  recseq  5859  tfr0  5875  tfrlemiex  5883  elinp  6449  prloc  6466  nnsub  7684  indstr  8261  ublbneg  8273  lbzbi  8276  iccsupr  8553  bj-omtrans  9009
  Copyright terms: Public domain W3C validator