Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  smufval Structured version   Unicode version

Theorem smufval 12994
 Description: Define the addition of two bit sequences, using df-had 1390 and df-cad 1391 bit operations. (Contributed by Mario Carneiro, 9-Sep-2016.)
Hypotheses
Ref Expression
smuval.a
smuval.b
Assertion
Ref Expression
smufval smul
Distinct variable groups:   ,,,,   ,,   ,,,,   ,
Allowed substitution hints:   (,)   (,,)

Proof of Theorem smufval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smuval.a . . 3
2 nn0ex 10232 . . . 4
32elpw2 4367 . . 3
41, 3sylibr 205 . 2
5 smuval.b . . 3
62elpw2 4367 . . 3
75, 6sylibr 205 . 2
8 simp1l 982 . . . . . . . . . . . . 13
98eleq2d 2505 . . . . . . . . . . . 12
10 simp1r 983 . . . . . . . . . . . . 13
1110eleq2d 2505 . . . . . . . . . . . 12
129, 11anbi12d 693 . . . . . . . . . . 11
1312rabbidv 2950 . . . . . . . . . 10
1413oveq2d 6100 . . . . . . . . 9 sadd sadd
1514mpt2eq3dva 6141 . . . . . . . 8 sadd sadd