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

Theorem ralbidv 2300
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 1398 . 2 xφ
2 ralbidv.1 . 2 (φ → (ψχ))
31, 2ralbid 2298 1 (φ → (x A ψx A χ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wral 2280
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 1312  ax-gen 1314  ax-4 1377  ax-17 1396
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-ral 2285
This theorem is referenced by:  ralbii  2304  2ralbidv  2322  rexralbidv  2324  r19.32vdc  2433  raleqbi1dv  2487  raleqbidv  2491  cbvral2v  2515  rspc2  2634  rspc3v  2638  reu6i  2705  reu7  2709  sbcralt  2807  sbcralg  2809  raaanlem  3301  r19.12sn  3406  2ralunsn  3539  elintg  3593  elintrabg  3598  eliin  3632  bnd2  3896  poeq1  4006  soeq1  4022  reusv3  4138  posng  4335  ralxpf  4405  cnvpom  4783  funcnvuni  4890  dff4im  5234  dff13f  5330  eusvobj2  5418  ofreq  5634  smoeq  5823  recseq  5839  tfrlemiex  5862  elinp  6322  prloc  6339  bj-omtrans  7401
  Copyright terms: Public domain W3C validator