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

Theorem spi 1767
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 1762 . 2
31, 2ax-mp 5 1
Colors of variables: wff set class
Syntax hints:  A.wal 1556
This theorem is referenced by:  darii  2425  barbari  2427  cesare  2429  camestres  2430  festino  2431  baroco  2432  cesaro  2433  camestros  2434  datisi  2435  disamis  2436  felapton  2439  darapti  2440  calemes  2441  dimatis  2442  fresison  2443  calemos  2444  fesapo  2445  bamalip  2446  kmlem2  8145  axac2  8460  axac  8461  axaci  8462  bnj864  30486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-12 1760
This theorem depends on definitions:  df-bi 179  df-ex 1558
  Copyright terms: Public domain W3C validator