Theorem sp 1488

Description: Specialization. Another name for ax-4 1487. (Contributed by NM, 21-May-2008.)

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

Step	Hyp	Ref	Expression
1		ax-4 1487	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4  ∀wal 1329

This theorem was proved from axioms:  ax-4 1487

This theorem is referenced by:  axi12  1494  nfr  1498  sps  1517  spsd  1518  19.3  1533  cbv1h  1723  nfald  1733  dveeq2  1787  nfsbxy  1913  nfsbxyt  1914  nfcr  2271  rsp  2478  ceqex  2807  abidnf  2847  mob2  2859  csbie2t  3043  sbcnestgf  3046  mpteq12f  4003  dtruarb  4110  copsex2t  4162  ssopab2  4192  eusv1  4368  alxfr  4377  eunex  4471  iota1  5097  fiintim  6810  genprndl  7322  genprndu  7323  fiinopn  12160  bdel  13032  bdsepnft  13074  strcollnft  13171