Theorem sp 1471

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

Syntax hints:   -> wi 4   A.wal 1312

This theorem was proved from axioms:  ax-4 1470

This theorem is referenced by:  axi12  1477  nfr  1481  sps  1500  spsd  1501  19.3  1516  cbv1h  1706  nfald  1716  dveeq2  1769  nfsbxy  1893  nfsbxyt  1894  nfcr  2247  rsp  2454  ceqex  2782  abidnf  2821  mob2  2833  csbie2t  3014  sbcnestgf  3017  mpteq12f  3968  dtruarb  4075  copsex2t  4127  ssopab2  4157  eusv1  4333  alxfr  4342  eunex  4436  iota1  5060  fiintim  6770  genprndl  7277  genprndu  7278  fiinopn  12014  bdel  12735  bdsepnft  12777  strcollnft  12874