![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > bdnthALT | GIF version |
Description: Alternate proof of bdnth 14506 not using bdfal 14505. Then, bdfal 14505 can be proved from this theorem, using fal 1360. The total number of proof steps would be 17 (for bdnthALT 14507) + 3 = 20, which is more than 8 (for bdfal 14505) + 9 (for bdnth 14506) = 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 14504 | . . 3 ⊢ BOUNDED ⊤ | |
2 | 1 | ax-bdn 14489 | . 2 ⊢ BOUNDED ¬ ⊤ |
3 | notnot 629 | . . . 4 ⊢ (⊤ → ¬ ¬ ⊤) | |
4 | 3 | mptru 1362 | . . 3 ⊢ ¬ ¬ ⊤ |
5 | bdnth.1 | . . 3 ⊢ ¬ 𝜑 | |
6 | 4, 5 | 2false 701 | . 2 ⊢ (¬ ⊤ ↔ 𝜑) |
7 | 2, 6 | bd0 14496 | 1 ⊢ BOUNDED 𝜑 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ⊤wtru 1354 BOUNDED wbd 14484 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-bd0 14485 ax-bdim 14486 ax-bdn 14489 ax-bdeq 14492 |
This theorem depends on definitions: df-bi 117 df-tru 1356 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |