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

Theorem spi 1501
Description: Inference reversing generalization (specialization). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
spi.1 𝑥𝜑
Assertion
Ref Expression
spi 𝜑

Proof of Theorem spi
StepHypRef Expression
1 spi.1 . 2 𝑥𝜑
2 ax-4 1472 . 2 (∀𝑥𝜑𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff set class
Syntax hints:  wal 1314
This theorem was proved from axioms:  ax-mp 5  ax-4 1472
This theorem is referenced by:  19.8a  1554  darii  2077  barbari  2079  cesare  2081  camestres  2082  festino  2083  baroco  2084  cesaro  2085  camestros  2086  datisi  2087  disamis  2088  felapton  2091  darapti  2092  calemes  2093  dimatis  2094  fresison  2095  calemos  2096  fesapo  2097  bamalip  2098  tfi  4466  acexmid  5741  bdsep1  13010  strcoll2  13108  sscoll2  13113
  Copyright terms: Public domain W3C validator