Theorem bdnthALT 16605

Description: Alternate proof of bdnth 16604 not using bdfal 16603. Then, bdfal 16603 can be proved from this theorem, using fal 1405. The total number of proof steps would be 17 (for bdnthALT 16605) + 3 = 20, which is more than 8 (for bdfal 16603) + 9 (for bdnth 16604) = 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 16602	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 16587	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 634	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	mptru 1407	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 709	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 16594	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1399  BOUNDED wbd 16582

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 619  ax-in2 620  ax-bd0 16583  ax-bdim 16584  ax-bdn 16587  ax-bdeq 16590

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

This theorem is referenced by: (None)