Theorem bdnthALT 9955

Description: Alternate proof of bdnth 9954 not using bdfal 9953. Then, bdfal 9953 can be proved from this theorem, using fal 1250. The total number of proof steps would be 17 (for bdnthALT 9955) + 3 = 20, which is more than 8 (for bdfal 9953) + 9 (for bdnth 9954) = 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 9952	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 9937	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 559	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	trud 1252	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 617	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 9944	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1244  BOUNDED wbd 9932

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-bd0 9933  ax-bdim 9934  ax-bdn 9937  ax-bdeq 9940

This theorem depends on definitions:  df-bi 110  df-tru 1246

This theorem is referenced by: (None)