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

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

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1521 1 (∀𝑥𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1362
This theorem was proved from axioms:  ax-4 1521
This theorem is referenced by:  axi12  1525  nfr  1529  sps  1548  spsd  1549  19.3  1565  cbv1h  1757  nfald  1771  dveeq2  1826  nfsbxy  1954  nfsbxyt  1955  nfcr  2324  nfabdw  2351  rsp  2537  ceqex  2879  abidnf  2920  mob2  2932  csbie2t  3120  sbcnestgf  3123  mpteq12f  4098  dtruarb  4209  copsex2t  4263  ssopab2  4293  eusv1  4470  alxfr  4479  eunex  4578  iota1  5210  fiintim  6958  genprndl  7551  genprndu  7552  fiinopn  13981  bdel  15075  bdsepnft  15117  strcollnft  15214
  Copyright terms: Public domain W3C validator