![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > bdnthALT | GIF version |
Description: Alternate proof of bdnth 13203 not using bdfal 13202. Then, bdfal 13202 can be proved from this theorem, using fal 1339. The total number of proof steps would be 17 (for bdnthALT 13204) + 3 = 20, which is more than 8 (for bdfal 13202) + 9 (for bdnth 13203) = 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 13201 | . . 3 ⊢ BOUNDED ⊤ | |
2 | 1 | ax-bdn 13186 | . 2 ⊢ BOUNDED ¬ ⊤ |
3 | notnot 619 | . . . 4 ⊢ (⊤ → ¬ ¬ ⊤) | |
4 | 3 | mptru 1341 | . . 3 ⊢ ¬ ¬ ⊤ |
5 | bdnth.1 | . . 3 ⊢ ¬ 𝜑 | |
6 | 4, 5 | 2false 691 | . 2 ⊢ (¬ ⊤ ↔ 𝜑) |
7 | 2, 6 | bd0 13193 | 1 ⊢ BOUNDED 𝜑 |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ⊤wtru 1333 BOUNDED wbd 13181 |
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 13182 ax-bdim 13183 ax-bdn 13186 ax-bdeq 13189 |
This theorem depends on definitions: df-bi 116 df-tru 1335 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |