![]() |
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 184 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bicomi 132 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3bitrri 207 3bitr2ri 209 3bitr4ri 213 nan 692 pm4.15 694 3or6 1323 sbal1yz 2001 2exsb 2009 moanim 2100 2eu4 2119 cvjust 2172 abbi 2291 sbc8g 2970 ss2rab 3231 unass 3292 unss 3309 undi 3383 difindiss 3389 notm0 3443 disj 3471 unopab 4079 eqvinop 4240 pwexb 4471 dmun 4830 reldm0 4841 dmres 4924 imadmrn 4976 ssrnres 5067 dmsnm 5090 coundi 5126 coundir 5127 cnvpom 5167 xpcom 5171 fun11 5279 fununi 5280 funcnvuni 5281 isarep1 5298 fsn 5684 fconstfvm 5730 eufnfv 5742 acexmidlem2 5866 eloprabga 5956 funoprabg 5968 ralrnmpo 5983 rexrnmpo 5984 oprabrexex2 6125 dfer2 6530 euen1b 6797 xpsnen 6815 rexuz3 10983 tgval2 13218 ssntr 13289 metrest 13673 sinhalfpilem 13879 |
Copyright terms: Public domain | W3C validator |