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

Theorem spi 1407
Description: Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
spi.1 xφ
Assertion
Ref Expression
spi φ

Proof of Theorem spi
StepHypRef Expression
1 spi.1 . 2 xφ
2 ax-4 1377 . 2 (xφφ)
31, 2ax-mp 7 1 φ
Colors of variables: wff set class
Syntax hints:  wal 1224
This theorem was proved from axioms:  ax-mp 7  ax-4 1377
This theorem is referenced by:  19.8a  1460  darii  1978  barbari  1980  cesare  1982  camestres  1983  festino  1984  baroco  1985  cesaro  1986  camestros  1987  datisi  1988  disamis  1989  felapton  1992  darapti  1993  calemes  1994  dimatis  1995  fresison  1996  calemos  1997  fesapo  1998  bamalip  1999  tfi  4228  acexmid  5431  bdsep2  7251  strcoll2  7340  sscoll2  7345
  Copyright terms: Public domain W3C validator