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 681 pm4.15 683 3or6 1301 sbal1yz 1974 2exsb 1982 moanim 2071 2eu4 2090 cvjust 2132 abbi 2251 sbc8g 2911 ss2rab 3168 unass 3228 unss 3245 undi 3319 difindiss 3325 notm0 3378 disj 3406 unopab 4002 eqvinop 4160 pwexb 4390 dmun 4741 reldm0 4752 dmres 4835 imadmrn 4886 ssrnres 4976 dmsnm 4999 coundi 5035 coundir 5036 cnvpom 5076 xpcom 5080 fun11 5185 fununi 5186 funcnvuni 5187 isarep1 5204 fsn 5585 fconstfvm 5631 eufnfv 5641 acexmidlem2 5764 eloprabga 5851 funoprabg 5863 ralrnmpo 5878 rexrnmpo 5879 oprabrexex2 6021 dfer2 6423 euen1b 6690 xpsnen 6708 rexuz3 10755 tgval2 12209 ssntr 12280 metrest 12664 sinhalfpilem 12861 |
Copyright terms: Public domain | W3C validator |