![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr3i | Unicode version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
Ref | Expression |
---|---|
3bitr3i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr3i.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr3i.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr3i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr3i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr3i 186 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr3i.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitri 184 |
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 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: an12 561 cbval2 1921 cbvex2 1922 sbco2vh 1945 equsb3 1951 sbn 1952 sbim 1953 sbor 1954 sban 1955 sbco2h 1964 sbco2d 1966 sbco2vd 1967 sbcomv 1971 sbco3 1974 sbcom 1975 sbcom2v 1985 sbcom2v2 1986 sbcom2 1987 dfsb7 1991 sb7f 1992 sb7af 1993 sbal 2000 sbex 2004 sbco4lem 2006 moanim 2100 eq2tri 2237 eqsb1 2281 clelsb1 2282 clelsb2 2283 clelsb1f 2323 ralcom4 2759 rexcom4 2760 ceqsralt 2764 gencbvex 2783 gencbval 2785 ceqsrexbv 2868 euind 2924 reuind 2942 sbccomlem 3037 sbccom 3038 raaan 3529 elxp2 4644 eqbrriv 4721 dm0rn0 4844 dfres2 4959 qfto 5018 xpm 5050 rninxp 5072 fununi 5284 dfoprab2 5921 dfer2 6535 euen1 6801 xpsnen 6820 xpassen 6829 enq0enq 7429 prnmaxl 7486 prnminu 7487 suplocexprlemell 7711 |
Copyright terms: Public domain | W3C validator |