Theorem bdnthALT 16222

Description: Alternate proof of bdnth 16221 not using bdfal 16220. Then, bdfal 16220 can be proved from this theorem, using fal 1402. The total number of proof steps would be 17 (for bdnthALT 16222) + 3 = 20, which is more than 8 (for bdfal 16220) + 9 (for bdnth 16221) = 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 16219	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 16204	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 632	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	mptru 1404	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 706	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 16211	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1396  BOUNDED wbd 16199

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 617  ax-in2 618  ax-bd0 16200  ax-bdim 16201  ax-bdn 16204  ax-bdeq 16207

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

This theorem is referenced by: (None)