Theorem sp 1441

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1282

This theorem was proved from axioms:  ax-4 1440

This theorem is referenced by:  axi12  1447  nfr  1451  sps  1470  spsd  1471  19.3  1486  cbv1h  1673  nfald  1683  dveeq2  1736  nfsbxy  1859  nfsbxyt  1860  nfcr  2211  rsp  2411  ceqex  2722  abidnf  2760  mob2  2772  csbie2t  2950  sbcnestgf  2953  mpteq12f  3858  dtruarb  3962  copsex2t  4000  ssopab2  4030  eusv1  4202  alxfr  4211  eunex  4304  iota1  4901  genprndl  6711  genprndu  6712  bdel  10636  bdsepnft  10678  strcollnft  10779