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  2931  abidnf  2972  mob2  2984  csbie2t  3174  sbcnestgf  3177  mpteq12f  4167  dtruarb  4279  copsex2t  4335  ssopab2  4368  eusv1  4547  alxfr  4556  eunex  4657  iota1  5299  fiintim  7116  genprndl  7731  genprndu  7732  fiinopn  14718  bdel  16376  bdsepnft  16418  strcollnft  16515