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

Theorem spv 1860
Description: Specialization, using implicit substitition. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
spv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
spv  |-  ( A. x ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x, y)    ps( y)

Proof of Theorem spv
StepHypRef Expression
1 spv.1 . . 3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
21biimpd 144 . 2  |-  ( x  =  y  ->  ( ph  ->  ps ) )
32spimv 1811 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wal 1351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  spvv  1907  cbvalvw  1919  chvarv  1937  ru  2961  nalset  4130  tfisi  4582  tfr1onlemsucfn  6334  tfr1onlemsucaccv  6335  tfr1onlembxssdm  6337  tfr1onlembfn  6338  tfr1onlemres  6343  tfri1dALT  6345  tfrcllemsucfn  6347  tfrcllemsucaccv  6348  tfrcllembxssdm  6350  tfrcllembfn  6351  tfrcllemres  6356  findcard2  6882  findcard2s  6883  bj-nalset  14269
  Copyright terms: Public domain W3C validator