Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  spi Structured version   Unicode version

Theorem spi 1770
 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 sp 1764 . 2
31, 2ax-mp 5 1
 Colors of variables: wff set class Syntax hints:  wal 1550 This theorem is referenced by:  darii  2382  barbari  2384  cesare  2386  camestres  2387  festino  2388  baroco  2389  cesaro  2390  camestros  2391  datisi  2392  disamis  2393  felapton  2396  darapti  2397  calemes  2398  dimatis  2399  fresison  2400  calemos  2401  fesapo  2402  bamalip  2403  kmlem2  8036  axac2  8351  axac  8352  axaci  8353  bnj864  29367 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762 This theorem depends on definitions:  df-bi 179  df-ex 1552
 Copyright terms: Public domain W3C validator