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

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

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1455 1 (∀𝑥𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1297
This theorem was proved from axioms:  ax-4 1455
This theorem is referenced by:  axi12  1462  nfr  1466  sps  1485  spsd  1486  19.3  1501  cbv1h  1691  nfald  1701  dveeq2  1754  nfsbxy  1878  nfsbxyt  1879  nfcr  2232  rsp  2439  ceqex  2766  abidnf  2805  mob2  2817  csbie2t  2998  sbcnestgf  3001  mpteq12f  3948  dtruarb  4055  copsex2t  4105  ssopab2  4135  eusv1  4311  alxfr  4320  eunex  4414  iota1  5038  fiintim  6746  genprndl  7230  genprndu  7231  fiinopn  11953  bdel  12624  bdsepnft  12666  strcollnft  12767
  Copyright terms: Public domain W3C validator