Theorem bdnthALT 15885

Description: Alternate proof of bdnth 15884 not using bdfal 15883. Then, bdfal 15883 can be proved from this theorem, using fal 1380. The total number of proof steps would be 17 (for bdnthALT 15885) + 3 = 20, which is more than 8 (for bdfal 15883) + 9 (for bdnth 15884) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
bdnth.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
bdnthALT	⊢ BOUNDED 𝜑

Proof of Theorem bdnthALT

Step	Hyp	Ref	Expression
1		bdtru 15882	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 15867	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 630	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	mptru 1382	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 703	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 15874	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1374  BOUNDED wbd 15862

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 615  ax-in2 616  ax-bd0 15863  ax-bdim 15864  ax-bdn 15867  ax-bdeq 15870

This theorem depends on definitions:  df-bi 117  df-tru 1376

This theorem is referenced by: (None)