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

Theorem spi 1470
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 ax-4 1441 . 2  |-  ( A. x ph  ->  ph )
31, 2ax-mp 7 1  |-  ph
Colors of variables: wff set class
Syntax hints:   A.wal 1283
This theorem was proved from axioms:  ax-mp 7  ax-4 1441
This theorem is referenced by:  19.8a  1523  darii  2042  barbari  2044  cesare  2046  camestres  2047  festino  2048  baroco  2049  cesaro  2050  camestros  2051  datisi  2052  disamis  2053  felapton  2056  darapti  2057  calemes  2058  dimatis  2059  fresison  2060  calemos  2061  fesapo  2062  bamalip  2063  tfi  4331  acexmid  5542  bdsep1  10834  strcoll2  10936  sscoll2  10941
  Copyright terms: Public domain W3C validator