Theorem sp 1560

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-4 1559

This theorem is referenced by:  axi12  1563  nfr  1567  sps  1586  spsd  1587  19.3  1603  cbv1h  1794  nfald  1808  dveeq2  1863  nfsbxy  1995  nfsbxyt  1996  nfcr  2367  nfabdw  2394  rsp  2580  ceqex  2934  abidnf  2975  mob2  2987  csbie2t  3177  sbcnestgf  3180  mpteq12f  4174  dtruarb  4287  copsex2t  4343  ssopab2  4376  eusv1  4555  alxfr  4564  eunex  4665  iota1  5308  fiintim  7166  genprndl  7784  genprndu  7785  fiinopn  14798  bdel  16544  bdsepnft  16586  strcollnft  16683