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  4212  dtruarb  4330  copsex2t  4387  ssopab2  4420  eusv1  4600  alxfr  4609  eunex  4710  iota1  5355  fiintim  7242  genprndl  7894  genprndu  7895  fiinopn  15230  bdel  17076  bdsepnft  17118  strcollnft  17215  dfalseu2  17384