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

Theorem spi 1499
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 1470 . 2 (∀𝑥𝜑𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff set class
Syntax hints:  wal 1312
This theorem was proved from axioms:  ax-mp 5  ax-4 1470
This theorem is referenced by:  19.8a  1552  darii  2075  barbari  2077  cesare  2079  camestres  2080  festino  2081  baroco  2082  cesaro  2083  camestros  2084  datisi  2085  disamis  2086  felapton  2089  darapti  2090  calemes  2091  dimatis  2092  fresison  2093  calemos  2094  fesapo  2095  bamalip  2096  tfi  4464  acexmid  5739  bdsep1  12885  strcoll2  12983  sscoll2  12988
  Copyright terms: Public domain W3C validator