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

Theorem spi 1772
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 1766 . 2
31, 2ax-mp 5 1
Colors of variables: wff set class
Syntax hints:  A.wal 1550
This theorem is referenced by:  darii  2387  barbari  2389  cesare  2391  camestres  2392  festino  2393  baroco  2394  cesaro  2395  camestros  2396  datisi  2397  disamis  2398  felapton  2401  darapti  2402  calemes  2403  dimatis  2404  fresison  2405  calemos  2406  fesapo  2407  bamalip  2408  kmlem2  8082  axac2  8397  axac  8398  axaci  8399  bnj864  29534
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 1628  ax-9 1669  ax-8 1690  ax-11 1764
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator