![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr2i | Unicode version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr2i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr2i.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr2i.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr2i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr2i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr2i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr4i 187 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr2i.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitri 184 |
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: an13 563 sbanv 1889 sbexyz 2003 exists1 2122 euxfrdc 2925 euind 2926 rmo4 2932 rmo3f 2936 rmo3 3056 ddifstab 3269 opm 4236 uniuni 4453 rabxp 4665 eliunxp 4768 dmmrnm 4848 imadisj 4992 intirr 5017 resco 5135 funcnv3 5280 fncnv 5284 fun11 5285 fununi 5286 f1mpt 5774 mpomptx 5968 ixp0x 6728 mapsnen 6813 xpcomco 6828 enq0tr 7435 elq 9624 pythagtrip 12285 ntreq0 13671 tx1cn 13808 |
Copyright terms: Public domain | W3C validator |