Theorem sp 1525

Description: Specialization. Another name for ax-4 1524. (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 1524	1 |- ( A. x ph -> ph )

Syntax hints:   -> wi 4   A.wal 1362

This theorem was proved from axioms:  ax-4 1524

This theorem is referenced by:  axi12  1528  nfr  1532  sps  1551  spsd  1552  19.3  1568  cbv1h  1760  nfald  1774  dveeq2  1829  nfsbxy  1961  nfsbxyt  1962  nfcr  2331  nfabdw  2358  rsp  2544  ceqex  2891  abidnf  2932  mob2  2944  csbie2t  3133  sbcnestgf  3136  mpteq12f  4113  dtruarb  4224  copsex2t  4278  ssopab2  4310  eusv1  4487  alxfr  4496  eunex  4597  iota1  5233  fiintim  6992  genprndl  7588  genprndu  7589  fiinopn  14240  bdel  15491  bdsepnft  15533  strcollnft  15630