![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr2ri | 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 |
---|---|
3bitr2ri |
![]() ![]() ![]() ![]() ![]() ![]() |
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 | bitr2i 258 |
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: xorass 1434 ssrab 3493 copsex2gb 4950 relop 4990 dmopab3 5053 issref 5219 fununi 5659 dffv2 5953 dfsup2 7976 kmlem3 8600 recmulnq 9407 ovoliunlem1 22533 shne0i 27182 ssiun3 28251 cnvoprab 28383 ind1a 28916 bnj1304 29703 bnj1253 29898 dfrecs2 30788 icorempt2 31824 dalem20 33329 rp-isfinite6 36234 rababg 36250 |
Copyright terms: Public domain | W3C validator |