Theorem bdnthALT 14727

Description: Alternate proof of bdnth 14726 not using bdfal 14725. Then, bdfal 14725 can be proved from this theorem, using fal 1360. The total number of proof steps would be 17 (for bdnthALT 14727) + 3 = 20, which is more than 8 (for bdfal 14725) + 9 (for bdnth 14726) = 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 14724	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 14709	. 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 14716	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1354  BOUNDED wbd 14704

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 14705  ax-bdim 14706  ax-bdn 14709  ax-bdeq 14712

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

This theorem is referenced by: (None)