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  1996  nfsbxyt  1997  nfcr  2376  nfabdw  2403  rsp  2589  ceqex  2944  abidnf  2985  mob2  2997  csbie2t  3187  sbcnestgf  3190  mpteq12f  4190  dtruarb  4304  copsex2t  4361  ssopab2  4394  eusv1  4573  alxfr  4582  eunex  4683  iota1  5327  fiintim  7191  genprndl  7836  genprndu  7837  fiinopn  14869  bdel  16615  bdsepnft  16657  strcollnft  16754