![]() |
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 185 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr3i.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitri 183 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: an12 529 cbval2 1845 cbvex2 1846 sbco2v 1870 equsb3 1874 sbn 1875 sbim 1876 sbor 1877 sban 1878 sbco2h 1887 sbco2d 1889 sbco2vd 1890 sbcomv 1894 sbco3 1897 sbcom 1898 sbcom2v 1910 sbcom2v2 1911 sbcom2 1912 dfsb7 1916 sb7f 1917 sb7af 1918 sbal 1925 sbex 1929 sbco4lem 1931 moanim 2023 eq2tri 2148 eqsb3 2192 clelsb3 2193 clelsb4 2194 clelsb3f 2233 ralcom4 2644 rexcom4 2645 ceqsralt 2649 gencbvex 2668 gencbval 2670 ceqsrexbv 2751 euind 2805 reuind 2823 sbccomlem 2916 sbccom 2917 raaan 3394 elxp2 4472 eqbrriv 4548 dm0rn0 4668 dfres2 4779 qfto 4836 xpm 4868 rninxp 4889 fununi 5097 dfoprab2 5712 dfer2 6309 euen1 6575 xpsnen 6593 xpassen 6602 enq0enq 7053 prnmaxl 7110 prnminu 7111 |
Copyright terms: Public domain | W3C validator |