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

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

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1441 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1283
This theorem was proved from axioms:  ax-4 1441
This theorem is referenced by:  axi12  1448  nfr  1452  sps  1471  spsd  1472  19.3  1487  cbv1h  1674  nfald  1684  dveeq2  1737  nfsbxy  1860  nfsbxyt  1861  nfcr  2212  rsp  2412  ceqex  2723  abidnf  2761  mob2  2773  csbie2t  2951  sbcnestgf  2954  mpteq12f  3866  dtruarb  3970  copsex2t  4008  ssopab2  4038  eusv1  4210  alxfr  4219  eunex  4312  iota1  4911  genprndl  6773  genprndu  6774  bdel  10794  bdsepnft  10836  strcollnft  10937
  Copyright terms: Public domain W3C validator