Theorem sp 1499

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1341

This theorem was proved from axioms:  ax-4 1498

This theorem is referenced by:  axi12  1502  nfr  1506  sps  1525  spsd  1526  19.3  1542  cbv1h  1734  nfald  1748  dveeq2  1803  nfsbxy  1930  nfsbxyt  1931  nfcr  2300  nfabdw  2327  rsp  2513  ceqex  2853  abidnf  2894  mob2  2906  csbie2t  3093  sbcnestgf  3096  mpteq12f  4062  dtruarb  4170  copsex2t  4223  ssopab2  4253  eusv1  4430  alxfr  4439  eunex  4538  iota1  5167  fiintim  6894  genprndl  7462  genprndu  7463  fiinopn  12642  bdel  13727  bdsepnft  13769  strcollnft  13866