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  4164  dtruarb  4275  copsex2t  4331  ssopab2  4364  eusv1  4543  alxfr  4552  eunex  4653  iota1  5293  fiintim  7104  genprndl  7719  genprndu  7720  fiinopn  14693  bdel  16263  bdsepnft  16305  strcollnft  16402