Theorem sp 1442

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

Syntax hints:   -> wi 4   A.wal 1283

This theorem was proved from axioms:  ax-4 1441

This theorem is referenced by:  axi12  1448  nfr  1452  sps  1471  spsd  1472  19.3  1487  cbv1h  1674  nfald  1684  dveeq2  1737  nfsbxy  1860  nfsbxyt  1861  nfcr  2212  rsp  2412  ceqex  2723  abidnf  2761  mob2  2773  csbie2t  2951  sbcnestgf  2954  mpteq12f  3866  dtruarb  3970  copsex2t  4008  ssopab2  4038  eusv1  4210  alxfr  4219  eunex  4312  iota1  4911  genprndl  6773  genprndu  6774  bdel  10794  bdsepnft  10836  strcollnft  10937