Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  exbtwnzlemshrink Unicode version

Theorem exbtwnzlemshrink 9405
 Description: Lemma for exbtwnzlemex 9406. Shrinking the range around . (Contributed by Jim Kingdon, 10-May-2022.)
Hypotheses
Ref Expression
exbtwnzlemshrink.j
exbtwnzlemshrink.a
exbtwnzlemshrink.tri
Assertion
Ref Expression
exbtwnzlemshrink
Distinct variable groups:   ,,   ,,   ,   ,,
Allowed substitution hints:   ()   (,)

Proof of Theorem exbtwnzlemshrink
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 exbtwnzlemshrink.j . . 3
3 oveq2 5572 . . . . . . . 8
43breq2d 3817 . . . . . . 7
54anbi2d 452 . . . . . 6
65rexbidv 2374 . . . . 5
76anbi2d 452 . . . 4
87imbi1d 229 . . 3
9 oveq2 5572 . . . . . . . 8
109breq2d 3817 . . . . . . 7
1110anbi2d 452 . . . . . 6
1211rexbidv 2374 . . . . 5
1312anbi2d 452 . . . 4
1413imbi1d 229 . . 3
15 oveq2 5572 . . . . . . . 8
1615breq2d 3817 . . . . . . 7
1716anbi2d 452 . . . . . 6
1817rexbidv 2374 . . . . 5
1918anbi2d 452 . . . 4
2019imbi1d 229 . . 3
21 oveq2 5572 . . . . . . . 8
2221breq2d 3817 . . . . . . 7
2322anbi2d 452 . . . . . 6
2423rexbidv 2374 . . . . 5
2524anbi2d 452 . . . 4
2625imbi1d 229 . . 3
27 breq1 3808 . . . . . . 7
28 oveq1 5571 . . . . . . . 8
2928breq2d 3817 . . . . . . 7
3027, 29anbi12d 457 . . . . . 6
3130cbvrexv 2583 . . . . 5
3231biimpi 118 . . . 4