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