Theorem sp 1559

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1395

This theorem was proved from axioms:  ax-4 1558

This theorem is referenced by:  axi12  1562  nfr  1566  sps  1585  spsd  1586  19.3  1602  cbv1h  1794  nfald  1808  dveeq2  1863  nfsbxy  1995  nfsbxyt  1996  nfcr  2366  nfabdw  2393  rsp  2579  ceqex  2933  abidnf  2974  mob2  2986  csbie2t  3176  sbcnestgf  3179  mpteq12f  4169  dtruarb  4281  copsex2t  4337  ssopab2  4370  eusv1  4549  alxfr  4558  eunex  4659  iota1  5301  fiintim  7122  genprndl  7740  genprndu  7741  fiinopn  14727  bdel  16440  bdsepnft  16482  strcollnft  16579