Theorem sp 1533

Description: Specialization. Another name for ax-4 1532. (Contributed by NM, 21-May-2008.)

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

Step	Hyp	Ref	Expression
1		ax-4 1532	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4  ∀wal 1370

This theorem was proved from axioms:  ax-4 1532

This theorem is referenced by:  axi12  1536  nfr  1540  sps  1559  spsd  1560  19.3  1576  cbv1h  1768  nfald  1782  dveeq2  1837  nfsbxy  1969  nfsbxyt  1970  nfcr  2339  nfabdw  2366  rsp  2552  ceqex  2899  abidnf  2940  mob2  2952  csbie2t  3141  sbcnestgf  3144  mpteq12f  4123  dtruarb  4234  copsex2t  4288  ssopab2  4321  eusv1  4498  alxfr  4507  eunex  4608  iota1  5245  fiintim  7027  genprndl  7633  genprndu  7634  fiinopn  14418  bdel  15714  bdsepnft  15756  strcollnft  15853