NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  spi GIF version

Theorem spi 1753
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 sp 1747 . 2 (xφφ)
31, 2ax-mp 5 1 φ
Colors of variables: wff setvar class
Syntax hints:  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  darii  2303  barbari  2305  cesare  2307  camestres  2308  festino  2309  baroco  2310  cesaro  2311  camestros  2312  datisi  2313  disamis  2314  felapton  2317  darapti  2318  calemes  2319  dimatis  2320  fresison  2321  calemos  2322  fesapo  2323  bamalip  2324
  Copyright terms: Public domain W3C validator