Theorem sp 1522

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-4 1521

This theorem is referenced by:  axi12  1525  nfr  1529  sps  1548  spsd  1549  19.3  1565  cbv1h  1757  nfald  1771  dveeq2  1826  nfsbxy  1958  nfsbxyt  1959  nfcr  2328  nfabdw  2355  rsp  2541  ceqex  2888  abidnf  2929  mob2  2941  csbie2t  3130  sbcnestgf  3133  mpteq12f  4110  dtruarb  4221  copsex2t  4275  ssopab2  4307  eusv1  4484  alxfr  4493  eunex  4594  iota1  5230  fiintim  6987  genprndl  7583  genprndu  7584  fiinopn  14183  bdel  15407  bdsepnft  15449  strcollnft  15546