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

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

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1416 1 (∀𝑥𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257
This theorem was proved from axioms:  ax-4 1416
This theorem is referenced by:  axi12  1423  nfr  1427  sps  1446  spsd  1447  19.3  1462  cbv1h  1649  nfald  1659  dveeq2  1712  nfsbxy  1834  nfsbxyt  1835  nfcr  2186  rsp  2386  ceqex  2694  abidnf  2732  mob2  2744  csbie2t  2922  sbcnestgf  2925  mpteq12f  3865  dtruarb  3970  copsex2t  4010  ssopab2  4040  eusv1  4212  alxfr  4221  eunex  4313  iota1  4909  genprndl  6677  genprndu  6678  bdel  10352  bdsepnft  10394  strcollnft  10496
  Copyright terms: Public domain W3C validator