Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > bdnthALT | Unicode version |
Description: Alternate proof of bdnth 13420 not using bdfal 13419. Then, bdfal 13419 can be proved from this theorem, using fal 1342. The total number of proof steps would be 17 (for bdnthALT 13421) + 3 = 20, which is more than 8 (for bdfal 13419) + 9 (for bdnth 13420) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bdnth.1 |
Ref | Expression |
---|---|
bdnthALT | BOUNDED |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bdtru 13418 | . . 3 BOUNDED | |
2 | 1 | ax-bdn 13403 | . 2 BOUNDED |
3 | notnot 619 | . . . 4 | |
4 | 3 | mptru 1344 | . . 3 |
5 | bdnth.1 | . . 3 | |
6 | 4, 5 | 2false 691 | . 2 |
7 | 2, 6 | bd0 13410 | 1 BOUNDED |
Colors of variables: wff set class |
Syntax hints: wn 3 wtru 1336 BOUNDED wbd 13398 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-bd0 13399 ax-bdim 13400 ax-bdn 13403 ax-bdeq 13406 |
This theorem depends on definitions: df-bi 116 df-tru 1338 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |