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

Theorem spi 1775
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 1770 . 2
31, 2ax-mp 5 1
Colors of variables: wff set class
Syntax hints:  A.wal 1564
This theorem is referenced by:  darii  2433  barbari  2435  cesare  2437  camestres  2438  festino  2439  baroco  2440  cesaro  2441  camestros  2442  datisi  2443  disamis  2444  felapton  2447  darapti  2448  calemes  2449  dimatis  2450  fresison  2451  calemos  2452  fesapo  2453  bamalip  2454  kmlem2  8202  axac2  8517  axac  8518  axaci  8519  bnj864  30763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-12 1768
This theorem depends on definitions:  df-bi 179  df-ex 1566
  Copyright terms: Public domain W3C validator