Theorem sp 1557

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1393

This theorem was proved from axioms:  ax-4 1556

This theorem is referenced by:  axi12  1560  nfr  1564  sps  1583  spsd  1584  19.3  1600  cbv1h  1792  nfald  1806  dveeq2  1861  nfsbxy  1993  nfsbxyt  1994  nfcr  2364  nfabdw  2391  rsp  2577  ceqex  2930  abidnf  2971  mob2  2983  csbie2t  3173  sbcnestgf  3176  mpteq12f  4163  dtruarb  4274  copsex2t  4330  ssopab2  4363  eusv1  4542  alxfr  4551  eunex  4652  iota1  5292  fiintim  7089  genprndl  7704  genprndu  7705  fiinopn  14672  bdel  16166  bdsepnft  16208  strcollnft  16305