NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  albidv GIF version

Theorem albidv 1625
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 1616 . 2 (φxφ)
2 albidv.1 . 2 (φ → (ψχ))
31, 2albidh 1590 1 (φ → (xψxχ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  2albidv  1627  ax11wdemo  1723  ax11vALT  2097  sbcom2  2114  ax10-16  2190  eujust  2206  eujustALT  2207  euf  2210  mo  2226  axext3  2336  bm1.1  2338  eqeq1  2359  nfceqdf  2488  ralbidv2  2636  alexeq  2968  pm13.183  2979  eqeu  3007  mo2icl  3015  euind  3023  reuind  3039  sbcal  3093  sbcalg  3094  sbcabel  3123  csbiebg  3175  ssconb  3399  reldisj  3594  sbcss  3660  elint  3932  iota5  4359  nnadjoin  4520  sfintfin  4532  tfinnn  4534  spfinsfincl  4539  spfininduct  4540  ssrel  4844  funimass4  5368  dffo3  5422  dff13  5471  fnfullfunlem1  5856  frd  5922
  Copyright terms: Public domain W3C validator