![]() |
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 120 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | sbimi 1764 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | biimpri 133 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | sbimi 1764 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 126 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-sb 1763 |
This theorem is referenced by: sbco2vh 1945 equsb3 1951 sbn 1952 sbim 1953 sbor 1954 sban 1955 sb3an 1958 sbbi 1959 sbco2h 1964 sbco2d 1966 sbco2vd 1967 sbco3v 1969 sbco3 1974 sbcom2v2 1986 sbcom2 1987 dfsb7 1991 sb7f 1992 sb7af 1993 sbal 2000 sbal1 2002 sbex 2004 sbco4lem 2006 sbco4 2007 sbmo 2085 elsb1 2155 elsb2 2156 eqsb1 2281 clelsb1 2282 clelsb2 2283 cbvabw 2300 clelsb1f 2323 sbabel 2346 sbralie 2721 sbcco 2984 exss 4226 inopab 4758 isarep1 5301 bezoutlemnewy 11989 |
Copyright terms: Public domain | W3C validator |