Theorem bdnthALT 13870

Description: Alternate proof of bdnth 13869 not using bdfal 13868. Then, bdfal 13868 can be proved from this theorem, using fal 1355. The total number of proof steps would be 17 (for bdnthALT 13870) + 3 = 20, which is more than 8 (for bdfal 13868) + 9 (for bdnth 13869) = 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 13867	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 13852	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 624	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	mptru 1357	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 696	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 13859	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1349  BOUNDED wbd 13847

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 609  ax-in2 610  ax-bd0 13848  ax-bdim 13849  ax-bdn 13852  ax-bdeq 13855

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

This theorem is referenced by: (None)