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 186 | . 2 |
4 | 3bitr2i.3 | . 2 | |
5 | 3, 4 | bitri 183 | 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: an13 537 sbanv 1845 sbexyz 1956 exists1 2073 euxfrdc 2843 euind 2844 rmo4 2850 rmo3f 2854 rmo3 2972 ddifstab 3178 opm 4126 uniuni 4342 rabxp 4546 eliunxp 4648 dmmrnm 4728 imadisj 4871 intirr 4895 resco 5013 funcnv3 5155 fncnv 5159 fun11 5160 fununi 5161 f1mpt 5640 mpomptx 5830 ixp0x 6588 mapsnen 6673 xpcomco 6688 enq0tr 7210 elq 9382 ntreq0 12228 tx1cn 12365 |
Copyright terms: Public domain | W3C validator |