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 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4  ∀wal 1400

This theorem was proved from axioms:  ax-4 1563

This theorem is referenced 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  4206  dtruarb  4323  copsex2t  4380  ssopab2  4413  eusv1  4593  alxfr  4602  eunex  4703  iota1  5347  fiintim  7228  genprndl  7878  genprndu  7879  fiinopn  15028  bdel  16785  bdsepnft  16827  strcollnft  16924