Theorem sp 1444

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1285

This theorem was proved from axioms:  ax-4 1443

This theorem is referenced by:  axi12  1450  nfr  1454  sps  1473  spsd  1474  19.3  1489  cbv1h  1677  nfald  1687  dveeq2  1740  nfsbxy  1863  nfsbxyt  1864  nfcr  2217  rsp  2419  ceqex  2735  abidnf  2774  mob2  2786  csbie2t  2965  sbcnestgf  2968  mpteq12f  3895  dtruarb  4002  copsex2t  4048  ssopab2  4078  eusv1  4250  alxfr  4259  eunex  4352  iota1  4962  genprndl  7027  genprndu  7028  bdel  11205  bdsepnft  11247  strcollnft  11348