Theorem sp 1535

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

Syntax hints:   -> wi 4   A.wal 1371

This theorem was proved from axioms:  ax-4 1534

This theorem is referenced by:  axi12  1538  nfr  1542  sps  1561  spsd  1562  19.3  1578  cbv1h  1770  nfald  1784  dveeq2  1839  nfsbxy  1971  nfsbxyt  1972  nfcr  2342  nfabdw  2369  rsp  2555  ceqex  2907  abidnf  2948  mob2  2960  csbie2t  3150  sbcnestgf  3153  mpteq12f  4140  dtruarb  4251  copsex2t  4307  ssopab2  4340  eusv1  4517  alxfr  4526  eunex  4627  iota1  5265  fiintim  7054  genprndl  7669  genprndu  7670  fiinopn  14591  bdel  15980  bdsepnft  16022  strcollnft  16119