![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr2i | Structured version Visualization version 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 260 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr2i.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitri 257 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 190 |
This theorem is referenced by: con2bi 334 an13 813 xorneg2 1426 xorneg1OLD 1428 2eu4 2396 2eu5 2397 exists1 2401 euxfr 3236 euind 3237 rmo4 3243 2reu5lem3 3259 rmo3 3370 difin 3692 difin0ss 3845 reusv2lem4 4621 rabxp 4890 eliunxp 4991 imadisj 5206 intirr 5237 resco 5358 funcnv3 5666 fncnv 5669 fun11 5670 fununi 5671 mptfnf 5721 f1mpt 6187 mpt2mptx 6414 uniuni 6627 frxp 6933 oeeu 7330 ixp0x 7576 mapsnen 7673 xpcomco 7688 1sdom 7801 dffi3 7971 wemapsolem 8091 cardval3 8412 kmlem4 8609 kmlem12 8617 kmlem14 8619 kmlem15 8620 kmlem16 8621 fpwwe2 9094 axgroth4 9283 ltexprlem4 9490 bitsmod 14459 pythagtrip 14833 pgpfac1 17762 pgpfac 17766 isassa 18588 basdif0 20017 ntreq0 20142 tgcmp 20465 tx1cn 20673 rnelfmlem 21016 phtpcer 22075 caucfil 22302 minveclem1 22415 ovoliunlem1 22504 mdegleb 23062 istrkg2ld 24557 3v3e3cycl2 25441 iswwlk 25460 adjbd1o 27787 nmo 28170 rmo3f 28180 rmo4fOLD 28181 mpt2mptxf 28329 isros 29039 1stmbfm 29131 bnj976 29638 bnj1143 29651 bnj1533 29712 bnj864 29782 bnj983 29811 bnj1174 29861 bnj1175 29862 bnj1280 29878 cvmlift2lem12 30086 axacprim 30383 dfrecs2 30766 andnand1 31108 bj-dfssb2 31298 bj-denotes 31512 bj-snglc 31608 bj-dfmpt2a 31675 bj-mpt2mptALT 31676 mptsnunlem 31785 wl-cases2-dnf 31895 itg2addnc 32041 asindmre 32072 isopos 32791 dihglblem6 34953 dihglb2 34955 fgraphopab 36132 ifpid2g 36182 ifpim23g 36184 rp-fakeanorass 36202 elmapintrab 36227 relintabex 36232 relnonrel 36238 undmrnresiss 36255 elintima 36290 relexp0eq 36338 iunrelexp0 36339 dffrege115 36619 frege131 36635 frege133 36637 onfrALTlem5 36952 ndisj2 37427 ndmaovcom 38745 usgra2pth0 39942 eliunxp2 40388 mpt2mptx2 40389 alimp-no-surprise 40793 alsi-no-surprise 40808 |
Copyright terms: Public domain | W3C validator |