Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr2i | Unicode version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr2i.1 | |
bitr2i.2 |
Ref | Expression |
---|---|
bitr2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2i.1 | . . 3 | |
2 | bitr2i.2 | . . 3 | |
3 | 1, 2 | bitri 183 | . 2 |
4 | 3 | bicomi 131 | 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: 3bitrri 206 3bitr2ri 208 3bitr4ri 212 nan 682 pm4.15 684 3or6 1305 sbal1yz 1981 2exsb 1989 moanim 2080 2eu4 2099 cvjust 2152 abbi 2271 sbc8g 2944 ss2rab 3204 unass 3264 unss 3281 undi 3355 difindiss 3361 notm0 3414 disj 3442 unopab 4043 eqvinop 4203 pwexb 4434 dmun 4793 reldm0 4804 dmres 4887 imadmrn 4938 ssrnres 5028 dmsnm 5051 coundi 5087 coundir 5088 cnvpom 5128 xpcom 5132 fun11 5237 fununi 5238 funcnvuni 5239 isarep1 5256 fsn 5639 fconstfvm 5685 eufnfv 5697 acexmidlem2 5821 eloprabga 5908 funoprabg 5920 ralrnmpo 5935 rexrnmpo 5936 oprabrexex2 6078 dfer2 6481 euen1b 6748 xpsnen 6766 rexuz3 10890 tgval2 12462 ssntr 12533 metrest 12917 sinhalfpilem 13123 |
Copyright terms: Public domain | W3C validator |