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  1954  nfsbxyt  1955  nfcr  2324  nfabdw  2351  rsp  2537  ceqex  2879  abidnf  2920  mob2  2932  csbie2t  3120  sbcnestgf  3123  mpteq12f  4098  dtruarb  4209  copsex2t  4263  ssopab2  4293  eusv1  4470  alxfr  4479  eunex  4578  iota1  5210  fiintim  6958  genprndl  7551  genprndu  7552  fiinopn  13981  bdel  15075  bdsepnft  15117  strcollnft  15214