![]() |
Mathbox for Jarvin Udandy |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bothtbothsame | Structured version Visualization version Unicode version |
Description: Given both a, b are
equivalent to ![]() |
Ref | Expression |
---|---|
bothtbothsame.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
bothtbothsame.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bothtbothsame |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bothtbothsame.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | bothtbothsame.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr4i 256 |
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 189 |
This theorem is referenced by: mdandyv1 38532 mdandyv2 38533 mdandyv3 38534 mdandyv4 38535 mdandyv5 38536 mdandyv6 38537 mdandyv7 38538 mdandyv8 38539 mdandyv9 38540 mdandyv10 38541 mdandyv11 38542 mdandyv12 38543 mdandyv13 38544 mdandyv14 38545 mdandyv15 38546 dandysum2p2e4 38580 |
Copyright terms: Public domain | W3C validator |