Theorem bdnthALT 15491

Description: Alternate proof of bdnth 15490 not using bdfal 15489. Then, bdfal 15489 can be proved from this theorem, using fal 1371. The total number of proof steps would be 17 (for bdnthALT 15491) + 3 = 20, which is more than 8 (for bdfal 15489) + 9 (for bdnth 15490) = 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 15488	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 15473	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 630	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	mptru 1373	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 702	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 15480	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1365  BOUNDED wbd 15468

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 615  ax-in2 616  ax-bd0 15469  ax-bdim 15470  ax-bdn 15473  ax-bdeq 15476

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

This theorem is referenced by: (None)