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

Theorem spi 1765
Description: Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
spi.1  |-  A. x ph
Assertion
Ref Expression
spi  |-  ph

Proof of Theorem spi
StepHypRef Expression
1 spi.1 . 2  |-  A. x ph
2 sp 1759 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1546
This theorem is referenced by:  darii  2353  barbari  2355  cesare  2357  camestres  2358  festino  2359  baroco  2360  cesaro  2361  camestros  2362  datisi  2363  disamis  2364  felapton  2367  darapti  2368  calemes  2369  dimatis  2370  fresison  2371  calemos  2372  fesapo  2373  bamalip  2374  kmlem2  7987  axac2  8302  axac  8303  axaci  8304  bnj864  28999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator