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

Theorem spi 1426
Description: Inference rule reversing generalization. (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 1397 . 2
31, 2ax-mp 7 1
Colors of variables: wff set class
Syntax hints:  wal 1240
This theorem was proved from axioms:  ax-mp 7  ax-4 1397
This theorem is referenced by:  19.8a  1479  darii  1997  barbari  1999  cesare  2001  camestres  2002  festino  2003  baroco  2004  cesaro  2005  camestros  2006  datisi  2007  disamis  2008  felapton  2011  darapti  2012  calemes  2013  dimatis  2014  fresison  2015  calemos  2016  fesapo  2017  bamalip  2018  tfi  4248  acexmid  5454  bdsep2  9320  strcoll2  9413  sscoll2  9418
  Copyright terms: Public domain W3C validator