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

Theorem sp 1398
Description: Specialization. Another name for ax-4 1397. (Contributed by NM, 21-May-2008.)
Assertion
Ref Expression
sp

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1397 1
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1240
This theorem was proved from axioms:  ax-4 1397
This theorem is referenced by:  axi12  1404  nfr  1408  sps  1427  spsd  1428  19.3  1443  cbv1h  1630  nfald  1640  dveeq2  1693  nfsbxy  1815  nfsbxyt  1816  nfcr  2167  rsp  2363  ceqex  2665  abidnf  2703  mob2  2715  csbie2t  2888  sbcnestgf  2891  mpteq12f  3828  dtruarb  3933  copsex2t  3973  ssopab2  4003  eusv1  4150  alxfr  4159  eunex  4239  iota1  4824  genprndl  6503  genprndu  6504  bdel  9280  bdsepnft  9321  strcollnft  9414
  Copyright terms: Public domain W3C validator