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

Theorem sp 1444
Description: Specialization. Another name for ax-4 1443. (Contributed by NM, 21-May-2008.)
Assertion
Ref Expression
sp (∀𝑥𝜑𝜑)

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1443 1 (∀𝑥𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1285
This theorem was proved from axioms:  ax-4 1443
This theorem is referenced by:  axi12  1450  nfr  1454  sps  1473  spsd  1474  19.3  1489  cbv1h  1677  nfald  1687  dveeq2  1740  nfsbxy  1863  nfsbxyt  1864  nfcr  2217  rsp  2419  ceqex  2735  abidnf  2774  mob2  2786  csbie2t  2965  sbcnestgf  2968  mpteq12f  3895  dtruarb  4002  copsex2t  4048  ssopab2  4078  eusv1  4250  alxfr  4259  eunex  4352  iota1  4962  genprndl  7027  genprndu  7028  bdel  11205  bdsepnft  11247  strcollnft  11348
  Copyright terms: Public domain W3C validator