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: wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: an12 551 cbval2 1901 cbvex2 1902 sbco2vh 1925 equsb3 1931 sbn 1932 sbim 1933 sbor 1934 sban 1935 sbco2h 1944 sbco2d 1946 sbco2vd 1947 sbcomv 1951 sbco3 1954 sbcom 1955 sbcom2v 1965 sbcom2v2 1966 sbcom2 1967 dfsb7 1971 sb7f 1972 sb7af 1973 sbal 1980 sbex 1984 sbco4lem 1986 moanim 2080 eq2tri 2217 eqsb3 2261 clelsb3 2262 clelsb4 2263 clelsb3f 2303 ralcom4 2734 rexcom4 2735 ceqsralt 2739 gencbvex 2758 gencbval 2760 ceqsrexbv 2843 euind 2899 reuind 2917 sbccomlem 3011 sbccom 3012 raaan 3500 elxp2 4604 eqbrriv 4681 dm0rn0 4803 dfres2 4918 qfto 4975 xpm 5007 rninxp 5029 fununi 5238 dfoprab2 5868 dfer2 6481 euen1 6747 xpsnen 6766 xpassen 6775 enq0enq 7351 prnmaxl 7408 prnminu 7409 suplocexprlemell 7633 |
Copyright terms: Public domain | W3C validator |