Theorem: bitvec_AndOrXor_2243__B__C__A__B___B__A__C (Eval/bitvec_AndOrXor_2243__B__C__A__B___B__A__C.lean)

State before:
⊢ ∀ (A C B : BitVec 64), (B ||| C) &&& A ||| B = B ||| A &&& C
Tactic:
intros
State after:
A✝ C✝ B✝ : BitVec 64
⊢ (B✝ ||| C✝) &&& A✝ ||| B✝ = B✝ ||| A✝ &&& C✝

State before:
A✝ C✝ B✝ : BitVec 64
⊢ (B✝ ||| C✝) &&& A✝ ||| B✝ = B✝ ||| A✝ &&& C✝
Tactic:
bv_decide
State after:
no goals