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

Theorem sp 1511
Description: Specialization. Another name for ax-4 1510. (Contributed by NM, 21-May-2008.)
Assertion
Ref Expression
sp  |-  ( A. x ph  ->  ph )

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1510 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1351
This theorem was proved from axioms:  ax-4 1510
This theorem is referenced by:  axi12  1514  nfr  1518  sps  1537  spsd  1538  19.3  1554  cbv1h  1746  nfald  1760  dveeq2  1815  nfsbxy  1942  nfsbxyt  1943  nfcr  2311  nfabdw  2338  rsp  2524  ceqex  2864  abidnf  2905  mob2  2917  csbie2t  3105  sbcnestgf  3108  mpteq12f  4082  dtruarb  4190  copsex2t  4244  ssopab2  4274  eusv1  4451  alxfr  4460  eunex  4559  iota1  5191  fiintim  6925  genprndl  7517  genprndu  7518  fiinopn  13373  bdel  14457  bdsepnft  14499  strcollnft  14596
  Copyright terms: Public domain W3C validator