ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  spi Unicode version

Theorem spi 1516
Description: Inference reversing generalization (specialization). (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 ax-4 1487 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1329
This theorem was proved from axioms:  ax-mp 5  ax-4 1487
This theorem is referenced by:  19.8a  1569  darii  2097  barbari  2099  cesare  2101  camestres  2102  festino  2103  baroco  2104  cesaro  2105  camestros  2106  datisi  2107  disamis  2108  felapton  2111  darapti  2112  calemes  2113  dimatis  2114  fresison  2115  calemos  2116  fesapo  2117  bamalip  2118  tfi  4491  acexmid  5766  bdsep1  13072  strcoll2  13170  sscoll2  13175
  Copyright terms: Public domain W3C validator