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

Theorem albidv 1705
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 1419 . 2 (φxφ)
2 albidv.1 . 2 (φ → (ψχ))
31, 2albidh 1369 1 (φ → (xψxχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wal 1241
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 1336  ax-gen 1338  ax-17 1419
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11v  1708  2albidv  1747  sbal1yz  1877  eujust  1902  euf  1905  mo23  1941  axext3  2023  bm1.1  2025  eqeq1  2046  nfceqdf  2177  ralbidv2  2325  alexeq  2667  pm13.183  2678  eqeu  2708  mo2icl  2717  euind  2725  reuind  2741  cdeqal  2750  sbcal  2807  sbcalg  2808  sbcabel  2836  csbiebg  2886  ssconb  3073  reldisj  3268  sbcssg  3327  elint  3615  axsep2  3870  zfauscl  3871  bm1.3ii  3872  euotd  3985  eusv1  4153  regexmid  4222  tfisi  4256  nnregexmid  4288  iota5  4833  sbcfung  4871  funimass4  5170  dffo3  5260  eufnfv  5335  dff13  5353  ssfiexmid  6258  fz1sbc  8820  frecuzrdgfn  8971  bdsep2  9449  bdsepnfALT  9452  bdzfauscl  9453  bdbm1.3ii  9454  bj-2inf  9505  bj-nn0sucALT  9546  strcoll2  9551  strcollnfALT  9554
  Copyright terms: Public domain W3C validator