Theorem sp 1488

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1329

This theorem was proved from axioms:  ax-4 1487

This theorem is referenced by:  axi12  1494  nfr  1498  sps  1517  spsd  1518  19.3  1533  cbv1h  1723  nfald  1733  dveeq2  1787  nfsbxy  1915  nfsbxyt  1916  nfcr  2273  rsp  2480  ceqex  2812  abidnf  2852  mob2  2864  csbie2t  3048  sbcnestgf  3051  mpteq12f  4008  dtruarb  4115  copsex2t  4167  ssopab2  4197  eusv1  4373  alxfr  4382  eunex  4476  iota1  5102  fiintim  6817  genprndl  7329  genprndu  7330  fiinopn  12171  bdel  13043  bdsepnft  13085  strcollnft  13182