Theorem bdnthALT 13033

Description: Alternate proof of bdnth 13032 not using bdfal 13031. Then, bdfal 13031 can be proved from this theorem, using fal 1338. The total number of proof steps would be 17 (for bdnthALT 13033) + 3 = 20, which is more than 8 (for bdfal 13031) + 9 (for bdnth 13032) = 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 13030	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 13015	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 618	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	mptru 1340	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 690	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 13022	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1332  BOUNDED wbd 13010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-bd0 13011  ax-bdim 13012  ax-bdn 13015  ax-bdeq 13018

This theorem depends on definitions:  df-bi 116  df-tru 1334

This theorem is referenced by: (None)