Theorem sp 1525

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-4 1524

This theorem is referenced by:  axi12  1528  nfr  1532  sps  1551  spsd  1552  19.3  1568  cbv1h  1760  nfald  1774  dveeq2  1829  nfsbxy  1961  nfsbxyt  1962  nfcr  2331  nfabdw  2358  rsp  2544  ceqex  2891  abidnf  2932  mob2  2944  csbie2t  3133  sbcnestgf  3136  mpteq12f  4114  dtruarb  4225  copsex2t  4279  ssopab2  4311  eusv1  4488  alxfr  4497  eunex  4598  iota1  5234  fiintim  7001  genprndl  7605  genprndu  7606  fiinopn  14324  bdel  15575  bdsepnft  15617  strcollnft  15714