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  4125  dtruarb  4236  copsex2t  4290  ssopab2  4323  eusv1  4500  alxfr  4509  eunex  4610  iota1  5247  fiintim  7030  genprndl  7636  genprndu  7637  fiinopn  14509  bdel  15818  bdsepnft  15860  strcollnft  15957