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

Theorem spi 1474
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 1445 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 7 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1287
This theorem was proved from axioms:  ax-mp 7  ax-4 1445
This theorem is referenced by:  19.8a  1527  darii  2048  barbari  2050  cesare  2052  camestres  2053  festino  2054  baroco  2055  cesaro  2056  camestros  2057  datisi  2058  disamis  2059  felapton  2062  darapti  2063  calemes  2064  dimatis  2065  fresison  2066  calemos  2067  fesapo  2068  bamalip  2069  tfi  4387  acexmid  5633  bdsep1  11420  strcoll2  11522  sscoll2  11527
  Copyright terms: Public domain W3C validator