Theorem sp 1534

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

Syntax hints:   -> wi 4   A.wal 1371

This theorem was proved from axioms:  ax-4 1533

This theorem is referenced by:  axi12  1537  nfr  1541  sps  1560  spsd  1561  19.3  1577  cbv1h  1769  nfald  1783  dveeq2  1838  nfsbxy  1970  nfsbxyt  1971  nfcr  2340  nfabdw  2367  rsp  2553  ceqex  2900  abidnf  2941  mob2  2953  csbie2t  3142  sbcnestgf  3145  mpteq12f  4124  dtruarb  4235  copsex2t  4289  ssopab2  4322  eusv1  4499  alxfr  4508  eunex  4609  iota1  5246  fiintim  7028  genprndl  7634  genprndu  7635  fiinopn  14476  bdel  15785  bdsepnft  15827  strcollnft  15924