Theorem sp 1511

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

Syntax hints:   -> wi 4   A.wal 1351

This theorem was proved from axioms:  ax-4 1510

This theorem is referenced by:  axi12  1514  nfr  1518  sps  1537  spsd  1538  19.3  1554  cbv1h  1746  nfald  1760  dveeq2  1815  nfsbxy  1942  nfsbxyt  1943  nfcr  2311  nfabdw  2338  rsp  2524  ceqex  2864  abidnf  2905  mob2  2917  csbie2t  3105  sbcnestgf  3108  mpteq12f  4082  dtruarb  4190  copsex2t  4244  ssopab2  4274  eusv1  4451  alxfr  4460  eunex  4559  iota1  5191  fiintim  6925  genprndl  7517  genprndu  7518  fiinopn  13373  bdel  14457  bdsepnft  14499  strcollnft  14596