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 1744 | . 2 |
4 | 1 | biimpri 132 | . . 3 |
5 | 4 | sbimi 1744 | . 2 |
6 | 3, 5 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wsb 1742 |
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 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-sb 1743 |
This theorem is referenced by: sbco2vh 1925 equsb3 1931 sbn 1932 sbim 1933 sbor 1934 sban 1935 sb3an 1938 sbbi 1939 sbco2h 1944 sbco2d 1946 sbco2vd 1947 sbco3v 1949 sbco3 1954 sbcom2v2 1966 sbcom2 1967 dfsb7 1971 sb7f 1972 sb7af 1973 sbal 1980 sbal1 1982 sbex 1984 sbco4lem 1986 sbco4 1987 sbmo 2065 elsb3 2135 elsb4 2136 eqsb3 2261 clelsb3 2262 clelsb4 2263 cbvabw 2280 clelsb3f 2303 sbabel 2326 sbralie 2696 sbcco 2958 exss 4187 inopab 4718 isarep1 5256 bezoutlemnewy 11880 |
Copyright terms: Public domain | W3C validator |