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  1795  nfald  1809  dveeq2  1864  nfsbxy  1998  nfsbxyt  1999  nfcr  2378  nfabdw  2405  rsp  2591  ceqex  2947  abidnf  2988  mob2  3000  csbie2t  3190  sbcnestgf  3193  mpteq12f  4195  dtruarb  4309  copsex2t  4366  ssopab2  4399  eusv1  4578  alxfr  4587  eunex  4688  iota1  5332  fiintim  7204  genprndl  7852  genprndu  7853  fiinopn  14995  bdel  16741  bdsepnft  16783  strcollnft  16880