![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbbii | Unicode version |
Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sbbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sbbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbbii.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 119 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | sbimi 1738 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | biimpri 132 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | sbimi 1738 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 125 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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-ial 1515 |
This theorem depends on definitions: df-bi 116 df-sb 1737 |
This theorem is referenced by: sbco2vh 1919 equsb3 1925 sbn 1926 sbim 1927 sbor 1928 sban 1929 sb3an 1932 sbbi 1933 sbco2h 1938 sbco2d 1940 sbco2vd 1941 sbco3v 1943 sbco3 1948 elsb3 1952 elsb4 1953 sbcom2v2 1962 sbcom2 1963 dfsb7 1967 sb7f 1968 sb7af 1969 sbal 1976 sbal1 1978 sbex 1980 sbco4lem 1982 sbco4 1983 sbmo 2059 eqsb3 2244 clelsb3 2245 clelsb4 2246 cbvabw 2263 clelsb3f 2286 sbabel 2308 sbralie 2673 sbcco 2934 exss 4157 inopab 4679 isarep1 5217 bezoutlemnewy 11720 |
Copyright terms: Public domain | W3C validator |