Theorem sp 1522

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

Assertion

Ref	Expression
sp	|- ( A. x ph -> ph )

Proof of Theorem sp

Step	Hyp	Ref	Expression
1		ax-4 1521	1 |- ( A. x ph -> ph )

Syntax hints:   -> wi 4   A.wal 1362

This theorem was proved from axioms:  ax-4 1521

This theorem is referenced by:  axi12  1525  nfr  1529  sps  1548  spsd  1549  19.3  1565  cbv1h  1757  nfald  1771  dveeq2  1826  nfsbxy  1958  nfsbxyt  1959  nfcr  2328  nfabdw  2355  rsp  2541  ceqex  2887  abidnf  2928  mob2  2940  csbie2t  3129  sbcnestgf  3132  mpteq12f  4109  dtruarb  4220  copsex2t  4274  ssopab2  4306  eusv1  4483  alxfr  4492  eunex  4593  iota1  5229  fiintim  6985  genprndl  7581  genprndu  7582  fiinopn  14172  bdel  15337  bdsepnft  15379  strcollnft  15476