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

Theorem spv 1833
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 143 . 2  |-  ( x  =  y  ->  ( ph  ->  ps ) )
32spimv 1784 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wal 1330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515
This theorem depends on definitions:  df-bi 116  df-nf 1438
This theorem is referenced by:  spvv  1880  chvarv  1910  ru  2911  nalset  4065  tfisi  4508  tfr1onlemsucfn  6244  tfr1onlemsucaccv  6245  tfr1onlembxssdm  6247  tfr1onlembfn  6248  tfr1onlemres  6253  tfri1dALT  6255  tfrcllemsucfn  6257  tfrcllemsucaccv  6258  tfrcllembxssdm  6260  tfrcllembfn  6261  tfrcllemres  6266  findcard2  6790  findcard2s  6791  bj-nalset  13262
  Copyright terms: Public domain W3C validator