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 1737 | . 2 |
4 | 1 | biimpri 132 | . . 3 |
5 | 4 | sbimi 1737 | . 2 |
6 | 3, 5 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wsb 1735 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-sb 1736 |
This theorem is referenced by: sbco2vh 1918 equsb3 1924 sbn 1925 sbim 1926 sbor 1927 sban 1928 sb3an 1931 sbbi 1932 sbco2h 1937 sbco2d 1939 sbco2vd 1940 sbco3v 1942 sbco3 1947 elsb3 1951 elsb4 1952 sbcom2v2 1961 sbcom2 1962 dfsb7 1966 sb7f 1967 sb7af 1968 sbal 1975 sbal1 1977 sbex 1979 sbco4lem 1981 sbco4 1982 sbmo 2058 eqsb3 2243 clelsb3 2244 clelsb4 2245 cbvabw 2262 clelsb3f 2285 sbabel 2307 sbralie 2670 sbcco 2930 exss 4149 inopab 4671 isarep1 5209 bezoutlemnewy 11684 |
Copyright terms: Public domain | W3C validator |