Theorem sp 1564

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1400

This proof depends on axioms:  ax-4 1563

This theorem is used by:  axi12  1567  nfr  1571  sps  1590  spsd  1591  19.3  1607  cbv1h  1799  nfald  1813  dveeq2  1868  nfsbxy  2002  nfsbxyt  2003  nfcr  2384  nfabdw  2411  rsp  2597  ceqex  2953  abidnf  2994  mob2  3006  csbie2t  3196  sbcnestgf  3199  mpteq12f  4211  dtruarb  4328  copsex2t  4385  ssopab2  4418  eusv1  4598  alxfr  4607  eunex  4708  iota1  5352  fiintim  7238  genprndl  7888  genprndu  7889  fiinopn  15105  bdel  16871  bdsepnft  16913  strcollnft  17010  dfalseu2  17177