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

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
StepHypRef Expression
1 ax-4 1487 1 (∀𝑥𝜑𝜑)
Colors of variables: wff set class
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  1915  nfsbxyt  1916  nfcr  2273  rsp  2480  ceqex  2812  abidnf  2852  mob2  2864  csbie2t  3048  sbcnestgf  3051  mpteq12f  4011  dtruarb  4118  copsex2t  4170  ssopab2  4200  eusv1  4376  alxfr  4385  eunex  4479  iota1  5105  fiintim  6820  genprndl  7348  genprndu  7349  fiinopn  12197  bdel  13187  bdsepnft  13229  strcollnft  13326
  Copyright terms: Public domain W3C validator