Theorem sp 1504

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1346

This theorem was proved from axioms:  ax-4 1503

This theorem is referenced by:  axi12  1507  nfr  1511  sps  1530  spsd  1531  19.3  1547  cbv1h  1739  nfald  1753  dveeq2  1808  nfsbxy  1935  nfsbxyt  1936  nfcr  2304  nfabdw  2331  rsp  2517  ceqex  2857  abidnf  2898  mob2  2910  csbie2t  3097  sbcnestgf  3100  mpteq12f  4069  dtruarb  4177  copsex2t  4230  ssopab2  4260  eusv1  4437  alxfr  4446  eunex  4545  iota1  5174  fiintim  6906  genprndl  7483  genprndu  7484  fiinopn  12796  bdel  13880  bdsepnft  13922  strcollnft  14019