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

Theorem spv 1783
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 142 . 2  |-  ( x  =  y  ->  ( ph  ->  ps ) )
32spimv 1734 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   A.wal 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391
This theorem is referenced by:  chvarv  1855  ru  2823  nalset  3928  tfisi  4356  tfr1onlemsucfn  6009  tfr1onlemsucaccv  6010  tfr1onlembxssdm  6012  tfr1onlembfn  6013  tfr1onlemres  6018  tfri1dALT  6020  tfrcllemsucfn  6022  tfrcllemsucaccv  6023  tfrcllembxssdm  6025  tfrcllembfn  6026  tfrcllemres  6031  findcard2  6445  findcard2s  6446  bj-nalset  10953
  Copyright terms: Public domain W3C validator