Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr4ri | Unicode version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
Ref | Expression |
---|---|
3bitr4i.1 | |
3bitr4i.2 | |
3bitr4i.3 |
Ref | Expression |
---|---|
3bitr4ri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4i.2 | . 2 | |
2 | 3bitr4i.1 | . . 3 | |
3 | 3bitr4i.3 | . . 3 | |
4 | 2, 3 | bitr4i 186 | . 2 |
5 | 1, 4 | bitr2i 184 | 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: dcnnOLD 834 excxor 1356 sbequ8 1819 2sb5 1956 2sb6 1957 2sb5rf 1962 2sb6rf 1963 moabs 2046 moanim 2071 2eu4 2090 2eu7 2091 sb8ab 2259 risset 2461 reuind 2884 difundi 3323 indifdir 3327 unab 3338 inab 3339 rabeq0 3387 abeq0 3388 inssdif0im 3425 snprc 3583 snss 3644 unipr 3745 uni0b 3756 pwtr 4136 opm 4151 onintexmid 4482 elxp2 4552 opthprc 4585 xpiundir 4593 elvvv 4597 relun 4651 inopab 4666 difopab 4667 ralxpf 4680 rexxpf 4681 dmiun 4743 rniun 4944 cnvresima 5023 imaco 5039 fnopabg 5241 dff1o2 5365 idref 5651 imaiun 5654 opabex3d 6012 opabex3 6013 elixx3g 9677 elfz2 9790 elfzuzb 9793 divalgb 11611 1nprm 11784 alsconv 13235 |
Copyright terms: Public domain | W3C validator |