Theorem List for Intuitionistic Logic Explorer - 1901-2000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sbanv 1901* |
Version of sban 1967 where and
are distinct. (Contributed by
Jim Kingdon, 24-Dec-2017.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif) 
 ![] ]](rbrack.gif)    |
|
Theorem | sborv 1902* |
Version of sbor 1966 where and
are distinct. (Contributed by
Jim Kingdon, 3-Feb-2018.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sbi1v 1903* |
Forward direction of sbimv 1905. (Contributed by Jim Kingdon,
25-Dec-2017.)
|
   ![] ]](rbrack.gif)  
 
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sbi2v 1904* |
Reverse direction of sbimv 1905. (Contributed by Jim Kingdon,
18-Jan-2018.)
|
    ![] ]](rbrack.gif)   ![] ]](rbrack.gif) 
  ![] ]](rbrack.gif)     |
|
Theorem | sbimv 1905* |
Intuitionistic proof of sbim 1965 where and
are distinct.
(Contributed by Jim Kingdon, 18-Jan-2018.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sblimv 1906* |
Version of sblim 1969 where and
are distinct. (Contributed by
Jim Kingdon, 19-Jan-2018.)
|
       ![] ]](rbrack.gif)      ![] ]](rbrack.gif)    |
|
Theorem | pm11.53 1907* |
Theorem *11.53 in [WhiteheadRussell]
p. 164. (Contributed by Andrew
Salmon, 24-May-2011.)
|
               |
|
Theorem | exlimivv 1908* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
1-Aug-1995.)
|
         |
|
Theorem | exlimdvv 1909* |
Deduction from Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
31-Jul-1995.)
|
             |
|
Theorem | exlimddv 1910* |
Existential elimination rule of natural deduction. (Contributed by
Mario Carneiro, 15-Jun-2016.)
|
           |
|
Theorem | 19.27v 1911* |
Theorem 19.27 of [Margaris] p. 90.
(Contributed by NM, 3-Jun-2004.)
|
   
       |
|
Theorem | 19.28v 1912* |
Theorem 19.28 of [Margaris] p. 90.
(Contributed by NM, 25-Mar-2004.)
|
   
 
     |
|
Theorem | 19.36aiv 1913* |
Inference from Theorem 19.36 of [Margaris] p.
90. (Contributed by NM,
5-Aug-1993.)
|
         |
|
Theorem | 19.41v 1914* |
Special case of Theorem 19.41 of [Margaris] p.
90. (Contributed by NM,
5-Aug-1993.)
|
   
       |
|
Theorem | 19.41vv 1915* |
Theorem 19.41 of [Margaris] p. 90 with 2
quantifiers. (Contributed by
NM, 30-Apr-1995.)
|
               |
|
Theorem | 19.41vvv 1916* |
Theorem 19.41 of [Margaris] p. 90 with 3
quantifiers. (Contributed by
NM, 30-Apr-1995.)
|
                   |
|
Theorem | 19.41vvvv 1917* |
Theorem 19.41 of [Margaris] p. 90 with 4
quantifiers. (Contributed by
FL, 14-Jul-2007.)
|
         
             |
|
Theorem | 19.42v 1918* |
Special case of Theorem 19.42 of [Margaris] p.
90. (Contributed by NM,
5-Aug-1993.)
|
   
 
     |
|
Theorem | spvv 1919* |
Version of spv 1871 with a disjoint variable condition.
(Contributed by
BJ, 31-May-2019.)
|
         |
|
Theorem | chvarvv 1920* |
Version of chvarv 1949 with a disjoint variable condition.
(Contributed by
BJ, 31-May-2019.)
|
     |
|
Theorem | exdistr 1921* |
Distribution of existential quantifiers. (Contributed by NM,
9-Mar-1995.)
|
               |
|
Theorem | exdistrv 1922* |
Distribute a pair of existential quantifiers (over disjoint variables)
over a conjunction. Combination of 19.41v 1914 and 19.42v 1918. For a
version with fewer disjoint variable conditions but requiring more
axioms, see eeanv 1944. (Contributed by BJ, 30-Sep-2022.)
|
               |
|
Theorem | 19.42vv 1923* |
Theorem 19.42 of [Margaris] p. 90 with 2
quantifiers. (Contributed by
NM, 16-Mar-1995.)
|
               |
|
Theorem | 19.42vvv 1924* |
Theorem 19.42 of [Margaris] p. 90 with 3
quantifiers. (Contributed by
NM, 21-Sep-2011.)
|
                   |
|
Theorem | 19.42vvvv 1925* |
Theorem 19.42 of [Margaris] p. 90 with 4
quantifiers. (Contributed by
Jim Kingdon, 23-Nov-2019.)
|
         
 
           |
|
Theorem | exdistr2 1926* |
Distribution of existential quantifiers. (Contributed by NM,
17-Mar-1995.)
|
                   |
|
Theorem | 3exdistr 1927* |
Distribution of existential quantifiers. (Contributed by NM,
9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
       
             |
|
Theorem | 4exdistr 1928* |
Distribution of existential quantifiers. (Contributed by NM,
9-Mar-1995.)
|
                               |
|
Theorem | cbvalv 1929* |
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 5-Aug-1993.)
|
           |
|
Theorem | cbvexv 1930* |
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 5-Aug-1993.)
|
           |
|
Theorem | cbvalvw 1931* |
Change bound variable. See cbvalv 1929 for a version with fewer disjoint
variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1459.
(Revised by GG, 25-Aug-2024.)
|
           |
|
Theorem | cbvexvw 1932* |
Change bound variable. See cbvexv 1930 for a version with fewer disjoint
variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1459.
(Revised by GG, 25-Aug-2024.)
|
           |
|
Theorem | cbval2 1933* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro,
6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)
|
                         |
|
Theorem | cbvex2 1934* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro,
6-Oct-2016.)
|
                         |
|
Theorem | cbval2v 1935* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 4-Feb-2005.)
|
                 |
|
Theorem | cbvex2v 1936* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 26-Jul-1995.)
|
                 |
|
Theorem | cbvald 1937* |
Deduction used to change bound variables, using implicit substitution,
particularly useful in conjunction with dvelim 2029. (Contributed by NM,
2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf
Lammen, 13-May-2018.)
|
       
             |
|
Theorem | cbvexdh 1938* |
Deduction used to change bound variables, using implicit substitition,
particularly useful in conjunction with dvelim 2029. (Contributed by NM,
2-Jan-2002.) (Proof rewritten by Jim Kingdon, 30-Dec-2017.)
|
     
          
        |
|
Theorem | cbvexd 1939* |
Deduction used to change bound variables, using implicit substitution,
particularly useful in conjunction with dvelim 2029. (Contributed by NM,
2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof rewritten
by Jim Kingdon, 10-Jun-2018.)
|
       
             |
|
Theorem | cbvaldva 1940* |
Rule used to change the bound variable in a universal quantifier with
implicit substitution. Deduction form. (Contributed by David Moews,
1-May-2017.)
|
               |
|
Theorem | cbvexdva 1941* |
Rule used to change the bound variable in an existential quantifier with
implicit substitution. Deduction form. (Contributed by David Moews,
1-May-2017.)
|
               |
|
Theorem | cbvex4v 1942* |
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 26-Jul-1995.)
|
        
                      |
|
Theorem | eean 1943 |
Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.)
(Revised by Mario Carneiro, 6-Oct-2016.)
|
         
         |
|
Theorem | eeanv 1944* |
Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
|
               |
|
Theorem | eeeanv 1945* |
Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
(Proof shortened by Andrew Salmon, 25-May-2011.)
|
       
           |
|
Theorem | ee4anv 1946* |
Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)
|
                       |
|
Theorem | ee8anv 1947* |
Rearrange existential quantifiers. (Contributed by Jim Kingdon,
23-Nov-2019.)
|
                                       |
|
Theorem | nexdv 1948* |
Deduction for generalization rule for negated wff. (Contributed by NM,
5-Aug-1993.)
|
       |
|
Theorem | chvarv 1949* |
Implicit substitution of for into a
theorem. (Contributed
by NM, 20-Apr-1994.)
|
     |
|
1.4.5 More substitution theorems
|
|
Theorem | hbs1 1950* |
is not free in   ![] ]](rbrack.gif) when and are distinct.
(Contributed by NM, 5-Aug-1993.) (Proof by Jim Kingdon, 16-Dec-2017.)
(New usage is discouraged.)
|
   ![] ]](rbrack.gif)   
 ![] ]](rbrack.gif)   |
|
Theorem | nfs1v 1951* |
is not free in   ![] ]](rbrack.gif) when and are distinct.
(Contributed by Mario Carneiro, 11-Aug-2016.)
|
    ![] ]](rbrack.gif)  |
|
Theorem | sbhb 1952* |
Two ways of expressing " is (effectively) not free in ."
(Contributed by NM, 29-May-2009.)
|
          ![] ]](rbrack.gif)    |
|
Theorem | hbsbv 1953* |
This is a version of hbsb 1961 with an extra distinct variable constraint,
on and . (Contributed by Jim
Kingdon, 25-Dec-2017.)
|
       ![] ]](rbrack.gif)   
 ![] ]](rbrack.gif)   |
|
Theorem | nfsbxy 1954* |
Similar to hbsb 1961 but with an extra distinct variable
constraint, on
and . (Contributed by Jim
Kingdon, 19-Mar-2018.)
|
      ![] ]](rbrack.gif)  |
|
Theorem | nfsbxyt 1955* |
Closed form of nfsbxy 1954. (Contributed by Jim Kingdon, 9-May-2018.)
|
       
 ![] ]](rbrack.gif)   |
|
Theorem | sbco2vlem 1956* |
This is a version of sbco2 1977 where is distinct from and from
. It is a lemma
on the way to proving sbco2v 1960 which only
requires that
and be distinct.
(Contributed by Jim Kingdon,
25-Dec-2017.) Remove one disjoint variable condition. (Revised by Jim
Kingdon, 3-Feb-2018.)
|
       ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbco2vh 1957* |
This is a version of sbco2 1977 where is distinct from .
(Contributed by Jim Kingdon, 12-Feb-2018.)
|
       ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | nfsb 1958* |
If is not free in , it is not free in
  ![] ]](rbrack.gif) when
and are distinct. (Contributed
by Mario Carneiro,
11-Aug-2016.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
|
      ![] ]](rbrack.gif)  |
|
Theorem | nfsbv 1959* |
If is not free in , it is not free in
  ![] ]](rbrack.gif) when
is distinct from
and . Version of nfsb 1958
requiring
more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.)
Remove disjoint variable condition on  . (Revised
by Steven
Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by GG,
25-Aug-2024.)
|
      ![] ]](rbrack.gif)  |
|
Theorem | sbco2v 1960* |
Version of sbco2 1977 with disjoint variable conditions.
(Contributed by
Wolf Lammen, 29-Apr-2023.)
|
     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | hbsb 1961* |
If is not free in , it is not free in
  ![] ]](rbrack.gif) when
and are distinct. (Contributed
by NM, 12-Aug-1993.) (Proof
rewritten by Jim Kingdon, 22-Mar-2018.)
|
       ![] ]](rbrack.gif)   
 ![] ]](rbrack.gif)   |
|
Theorem | equsb3lem 1962* |
Lemma for equsb3 1963. (Contributed by NM, 4-Dec-2005.) (Proof
shortened
by Andrew Salmon, 14-Jun-2011.)
|
   ![] ]](rbrack.gif)   |
|
Theorem | equsb3 1963* |
Substitution applied to an atomic wff. (Contributed by Raph Levien and
FL, 4-Dec-2005.)
|
   ![] ]](rbrack.gif)   |
|
Theorem | sbn 1964 |
Negation inside and outside of substitution are equivalent.
(Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon,
3-Feb-2018.)
|
  
  ![] ]](rbrack.gif)   |
|
Theorem | sbim 1965 |
Implication inside and outside of substitution are equivalent.
(Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon,
3-Feb-2018.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sbor 1966 |
Logical OR inside and outside of substitution are equivalent.
(Contributed by NM, 29-Sep-2002.) (Proof rewritten by Jim Kingdon,
3-Feb-2018.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sban 1967 |
Conjunction inside and outside of a substitution are equivalent.
(Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon,
3-Feb-2018.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif) 
 ![] ]](rbrack.gif)    |
|
Theorem | sbrim 1968 |
Substitution with a variable not free in antecedent affects only the
consequent. (Contributed by NM, 5-Aug-1993.)
|
       ![] ]](rbrack.gif)      ![] ]](rbrack.gif)    |
|
Theorem | sblim 1969 |
Substitution with a variable not free in consequent affects only the
antecedent. (Contributed by NM, 14-Nov-2013.) (Revised by Mario
Carneiro, 4-Oct-2016.)
|
     ![] ]](rbrack.gif)      ![] ]](rbrack.gif)    |
|
Theorem | sb3an 1970 |
Conjunction inside and outside of a substitution are equivalent.
(Contributed by NM, 14-Dec-2006.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif) 
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sbbi 1971 |
Equivalence inside and outside of a substitution are equivalent.
(Contributed by NM, 5-Aug-1993.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sblbis 1972 |
Introduce left biconditional inside of a substitution. (Contributed by
NM, 19-Aug-1993.)
|
   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)      ![] ]](rbrack.gif)    |
|
Theorem | sbrbis 1973 |
Introduce right biconditional inside of a substitution. (Contributed by
NM, 18-Aug-1993.)
|
   ![] ]](rbrack.gif)     ![] ]](rbrack.gif)      ![] ]](rbrack.gif)    |
|
Theorem | sbrbif 1974 |
Introduce right biconditional inside of a substitution. (Contributed by
NM, 18-Aug-1993.)
|
       ![] ]](rbrack.gif)     ![] ]](rbrack.gif)       |
|
Theorem | sbco2yz 1975* |
This is a version of sbco2 1977 where is distinct from . It is
a lemma on the way to proving sbco2 1977 which has no distinct variable
constraints. (Contributed by Jim Kingdon, 19-Mar-2018.)
|
     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbco2h 1976 |
A composition law for substitution. (Contributed by NM, 30-Jun-1994.)
(Proof rewritten by Jim Kingdon, 19-Mar-2018.)
|
       ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbco2 1977 |
A composition law for substitution. (Contributed by NM, 30-Jun-1994.)
(Revised by Mario Carneiro, 6-Oct-2016.)
|
     ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbco2d 1978 |
A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
|
              
 
 ![] ]](rbrack.gif) 
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sbco2vd 1979* |
Version of sbco2d 1978 with a distinct variable constraint between
and .
(Contributed by Jim Kingdon, 19-Feb-2018.)
|
              
 
 ![] ]](rbrack.gif) 
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | sbco 1980 |
A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbco3v 1981* |
Version of sbco3 1986 with a distinct variable constraint between
and
. (Contributed
by Jim Kingdon, 19-Feb-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbcocom 1982 |
Relationship between composition and commutativity for substitution.
(Contributed by Jim Kingdon, 28-Feb-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbcomv 1983* |
Version of sbcom 1987 with a distinct variable constraint between
and
. (Contributed
by Jim Kingdon, 28-Feb-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbcomxyyz 1984* |
Version of sbcom 1987 with distinct variable constraints between
and
, and and . (Contributed by Jim Kingdon,
21-Mar-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbco3xzyz 1985* |
Version of sbco3 1986 with distinct variable constraints between
and
, and and . Lemma for proving sbco3 1986. (Contributed
by Jim Kingdon, 22-Mar-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbco3 1986 |
A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
(Proof rewritten by Jim Kingdon, 22-Mar-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbcom 1987 |
A commutativity law for substitution. (Contributed by NM, 27-May-1997.)
(Proof rewritten by Jim Kingdon, 22-Mar-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | nfsbt 1988* |
Closed form of nfsb 1958. (Contributed by Jim Kingdon, 9-May-2018.)
|
       
 ![] ]](rbrack.gif)   |
|
Theorem | nfsbd 1989* |
Deduction version of nfsb 1958. (Contributed by NM, 15-Feb-2013.)
|
           ![] ]](rbrack.gif)   |
|
Theorem | sb9v 1990* |
Like sb9 1991 but with a distinct variable constraint
between and
. (Contributed
by Jim Kingdon, 28-Feb-2018.)
|
     ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   |
|
Theorem | sb9 1991 |
Commutation of quantification and substitution variables. (Contributed
by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
|
     ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   |
|
Theorem | sb9i 1992 |
Commutation of quantification and substitution variables. (Contributed by
NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
|
     ![] ]](rbrack.gif)     ![] ]](rbrack.gif)   |
|
Theorem | sbnf2 1993* |
Two ways of expressing " is (effectively) not free in ."
(Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario
Carneiro, 6-Oct-2016.)
|
        
 ![] ]](rbrack.gif)   ![] ]](rbrack.gif)    |
|
Theorem | hbsbd 1994* |
Deduction version of hbsb 1961. (Contributed by NM, 15-Feb-2013.) (Proof
rewritten by Jim Kingdon, 23-Mar-2018.)
|
              
 
 ![] ]](rbrack.gif)     ![] ]](rbrack.gif)    |
|
Theorem | 2sb5 1995* |
Equivalence for double substitution. (Contributed by NM,
3-Feb-2005.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)           |
|
Theorem | 2sb6 1996* |
Equivalence for double substitution. (Contributed by NM,
3-Feb-2005.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)           |
|
Theorem | sbcom2v 1997* |
Lemma for proving sbcom2 1999. It is the same as sbcom2 1999 but with
additional distinct variable constraints on and , and on
and . (Contributed by Jim
Kingdon, 19-Feb-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbcom2v2 1998* |
Lemma for proving sbcom2 1999. It is the same as sbcom2v 1997 but removes
the distinct variable constraint on and . (Contributed by
Jim Kingdon, 19-Feb-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sbcom2 1999* |
Commutativity law for substitution. Used in proof of Theorem 9.7 of
[Megill] p. 449 (p. 16 of the preprint).
(Contributed by NM,
27-May-1997.) (Proof modified to be intuitionistic by Jim Kingdon,
19-Feb-2018.)
|
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
|
Theorem | sb6a 2000* |
Equivalence for substitution. (Contributed by NM, 5-Aug-1993.)
|
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)    |