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 553 sbanv 1876 sbexyz 1990 exists1 2109 euxfrdc 2907 euind 2908 rmo4 2914 rmo3f 2918 rmo3 3037 ddifstab 3249 opm 4206 uniuni 4423 rabxp 4635 eliunxp 4737 dmmrnm 4817 imadisj 4960 intirr 4984 resco 5102 funcnv3 5244 fncnv 5248 fun11 5249 fununi 5250 f1mpt 5733 mpomptx 5924 ixp0x 6683 mapsnen 6768 xpcomco 6783 enq0tr 7366 elq 9551 pythagtrip 12194 ntreq0 12679 tx1cn 12816 |
Copyright terms: Public domain | W3C validator |