ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sp GIF version

Theorem sp 1401
Description: Specialization. Another name for ax-4 1400. (Contributed by NM, 21-May-2008.)
Assertion
Ref Expression
sp (∀𝑥𝜑𝜑)

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1400 1 (∀𝑥𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1241
This theorem was proved from axioms:  ax-4 1400
This theorem is referenced by:  axi12  1407  nfr  1411  sps  1430  spsd  1431  19.3  1446  cbv1h  1633  nfald  1643  dveeq2  1696  nfsbxy  1818  nfsbxyt  1819  nfcr  2170  rsp  2369  ceqex  2671  abidnf  2709  mob2  2721  csbie2t  2894  sbcnestgf  2897  mpteq12f  3837  dtruarb  3942  copsex2t  3982  ssopab2  4012  eusv1  4184  alxfr  4193  eunex  4285  iota1  4881  genprndl  6619  genprndu  6620  bdel  9965  bdsepnft  10007  strcollnft  10109
  Copyright terms: Public domain W3C validator