Theorem sp 1535

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1371

This theorem was proved from axioms:  ax-4 1534

This theorem is referenced by:  axi12  1538  nfr  1542  sps  1561  spsd  1562  19.3  1578  cbv1h  1770  nfald  1784  dveeq2  1839  nfsbxy  1971  nfsbxyt  1972  nfcr  2341  nfabdw  2368  rsp  2554  ceqex  2904  abidnf  2945  mob2  2957  csbie2t  3146  sbcnestgf  3149  mpteq12f  4132  dtruarb  4243  copsex2t  4297  ssopab2  4330  eusv1  4507  alxfr  4516  eunex  4617  iota1  5255  fiintim  7043  genprndl  7654  genprndu  7655  fiinopn  14551  bdel  15919  bdsepnft  15961  strcollnft  16058