![]() |
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 2923 euind 2924 rmo4 2930 rmo3f 2934 rmo3 3054 ddifstab 3267 opm 4234 uniuni 4451 rabxp 4663 eliunxp 4766 dmmrnm 4846 imadisj 4990 intirr 5015 resco 5133 funcnv3 5278 fncnv 5282 fun11 5283 fununi 5284 f1mpt 5771 mpomptx 5965 ixp0x 6725 mapsnen 6810 xpcomco 6825 enq0tr 7432 elq 9620 pythagtrip 12277 ntreq0 13563 tx1cn 13700 |
Copyright terms: Public domain | W3C validator |