![]() |
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 2760 rexcom4 2761 ceqsralt 2765 gencbvex 2784 gencbval 2786 ceqsrexbv 2869 euind 2925 reuind 2943 sbccomlem 3038 sbccom 3039 raaan 3530 elxp2 4645 eqbrriv 4722 dm0rn0 4845 dfres2 4960 qfto 5019 xpm 5051 rninxp 5073 fununi 5285 dfoprab2 5922 dfer2 6536 euen1 6802 xpsnen 6821 xpassen 6830 enq0enq 7430 prnmaxl 7487 prnminu 7488 suplocexprlemell 7712 |
Copyright terms: Public domain | W3C validator |