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

Theorem albidv 1683
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
albidv.1 (φ → (ψχ))
Assertion
Ref Expression
albidv (φ → (xψxχ))
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   χ(x)

Proof of Theorem albidv
StepHypRef Expression
1 ax-17 1396 . 2 (φxφ)
2 albidv.1 . 2 (φ → (ψχ))
31, 2albidh 1345 1 (φ → (xψxχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wal 1224
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-17 1396
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11v  1686  2albidv  1725  sbal1yz  1855  eujust  1880  euf  1883  mo23  1919  axext3  2001  bm1.1  2003  eqeq1  2024  nfceqdf  2155  ralbidv2  2302  alexeq  2643  pm13.183  2654  eqeu  2684  mo2icl  2693  euind  2701  reuind  2717  cdeqal  2726  sbcal  2783  sbcalg  2784  sbcabel  2812  csbiebg  2862  ssconb  3049  reldisj  3244  sbcssg  3305  elint  3591  axsep2  3846  zfauscl  3847  bm1.3ii  3848  euotd  3961  eusv1  4130  regexmid  4199  tfisi  4233  nnregexmid  4265  iota5  4810  sbcfung  4847  funimass4  5145  dffo3  5235  eufnfv  5310  dff13  5328  bdsep2  7251  bdsepnfALT  7254  bdzfauscl  7255  bdbm1.3ii  7256  bj-2inf  7299  bj-nn0sucALT  7335  strcoll2  7340  strcollnfALT  7343
  Copyright terms: Public domain W3C validator