Theorem sp 1456

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1297

This theorem was proved from axioms:  ax-4 1455

This theorem is referenced by:  axi12  1462  nfr  1466  sps  1485  spsd  1486  19.3  1501  cbv1h  1691  nfald  1701  dveeq2  1754  nfsbxy  1878  nfsbxyt  1879  nfcr  2232  rsp  2439  ceqex  2766  abidnf  2805  mob2  2817  csbie2t  2998  sbcnestgf  3001  mpteq12f  3948  dtruarb  4055  copsex2t  4105  ssopab2  4135  eusv1  4311  alxfr  4320  eunex  4414  iota1  5038  fiintim  6746  genprndl  7230  genprndu  7231  fiinopn  11953  bdel  12624  bdsepnft  12666  strcollnft  12767