Theorem sp 1557

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

Syntax hints:   -> wi 4   A.wal 1393

This theorem was proved from axioms:  ax-4 1556

This theorem is referenced by:  axi12  1560  nfr  1564  sps  1583  spsd  1584  19.3  1600  cbv1h  1792  nfald  1806  dveeq2  1861  nfsbxy  1993  nfsbxyt  1994  nfcr  2364  nfabdw  2391  rsp  2577  ceqex  2930  abidnf  2971  mob2  2983  csbie2t  3173  sbcnestgf  3176  mpteq12f  4164  dtruarb  4275  copsex2t  4331  ssopab2  4364  eusv1  4543  alxfr  4552  eunex  4653  iota1  5293  fiintim  7093  genprndl  7708  genprndu  7709  fiinopn  14678  bdel  16208  bdsepnft  16250  strcollnft  16347