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 687 pm4.15 689 3or6 1318 sbal1yz 1994 2exsb 2002 moanim 2093 2eu4 2112 cvjust 2165 abbi 2284 sbc8g 2962 ss2rab 3223 unass 3284 unss 3301 undi 3375 difindiss 3381 notm0 3435 disj 3463 unopab 4068 eqvinop 4228 pwexb 4459 dmun 4818 reldm0 4829 dmres 4912 imadmrn 4963 ssrnres 5053 dmsnm 5076 coundi 5112 coundir 5113 cnvpom 5153 xpcom 5157 fun11 5265 fununi 5266 funcnvuni 5267 isarep1 5284 fsn 5668 fconstfvm 5714 eufnfv 5726 acexmidlem2 5850 eloprabga 5940 funoprabg 5952 ralrnmpo 5967 rexrnmpo 5968 oprabrexex2 6109 dfer2 6514 euen1b 6781 xpsnen 6799 rexuz3 10954 tgval2 12845 ssntr 12916 metrest 13300 sinhalfpilem 13506 |
Copyright terms: Public domain | W3C validator |