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

Theorem spv 1871
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 1822 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wal 1362
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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545
This theorem depends on definitions:  df-bi 117  df-nf 1472
This theorem is referenced by:  spvv  1919  cbvalvw  1931  chvarv  1949  ru  2976  nalset  4148  tfisi  4604  tfr1onlemsucfn  6366  tfr1onlemsucaccv  6367  tfr1onlembxssdm  6369  tfr1onlembfn  6370  tfr1onlemres  6375  tfri1dALT  6377  tfrcllemsucfn  6379  tfrcllemsucaccv  6380  tfrcllembxssdm  6382  tfrcllembfn  6383  tfrcllemres  6388  findcard2  6918  findcard2s  6919  bj-nalset  15125
  Copyright terms: Public domain W3C validator