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

Theorem 2shfti 12913
 Description: Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
Hypothesis
Ref Expression
shftfval.1
Assertion
Ref Expression
2shfti

Proof of Theorem 2shfti
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 shftfval.1 . . . . . . . . 9
21shftfval 12903 . . . . . . . 8
32breqd 4463 . . . . . . 7
4 ovex 6324 . . . . . . . 8
5 vex 3112 . . . . . . . 8
6 eleq1 2529 . . . . . . . . 9
7 oveq1 6303 . . . . . . . . . 10
87breq1d 4462 . . . . . . . . 9
96, 8anbi12d 710 . . . . . . . 8
10 breq2 4456 . . . . . . . . 9
1110anbi2d 703 . . . . . . . 8
12 eqid 2457 . . . . . . . 8
134, 5, 9, 11, 12brab 4775 . . . . . . 7
143, 13syl6bb 261 . . . . . 6
1514ad2antrr 725 . . . . 5
16 subcl 9842 . . . . . . . 8
1716biantrurd 508 . . . . . . 7
1817ancoms 453 . . . . . 6
1918adantll 713 . . . . 5
20 sub32 9876 . . . . . . . . 9
21 subsub4 9875 . . . . . . . . 9
2220, 21eqtr3d 2500 . . . . . . . 8
23223expb 1197 . . . . . . 7
2423ancoms 453 . . . . . 6
2524breq1d 4462 . . . . 5
2615, 19, 253bitr2d 281 . . . 4
2726pm5.32da 641 . . 3
2827opabbidv 4515 . 2
29 ovex 6324 . . . 4
3029shftfval 12903 . . 3