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

Theorem spi 1864
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 1859 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  A.wal 1393
This theorem is referenced by:  darii  2398  barbari  2400  cesare  2402  camestres  2403  festino  2404  baroco  2405  cesaro  2406  camestros  2407  datisi  2408  disamis  2409  felapton  2412  darapti  2413  calemes  2414  dimatis  2415  fresison  2416  calemos  2417  fesapo  2418  bamalip  2419  kmlem2  8552  axac2  8867  axac  8868  axaci  8869  bnj864  33980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator