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

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

Proof of Theorem sp
StepHypRef Expression
1 ax-4 1445 1  |-  ( A. x ph  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287
This theorem was proved from axioms:  ax-4 1445
This theorem is referenced by:  axi12  1452  nfr  1456  sps  1475  spsd  1476  19.3  1491  cbv1h  1680  nfald  1690  dveeq2  1743  nfsbxy  1866  nfsbxyt  1867  nfcr  2220  rsp  2423  ceqex  2742  abidnf  2781  mob2  2793  csbie2t  2974  sbcnestgf  2977  mpteq12f  3910  dtruarb  4017  copsex2t  4063  ssopab2  4093  eusv1  4265  alxfr  4274  eunex  4367  iota1  4981  genprndl  7059  genprndu  7060  bdel  11382  bdsepnft  11424  strcollnft  11525
  Copyright terms: Public domain W3C validator