Theorem bdnthALT 16451

Description: Alternate proof of bdnth 16450 not using bdfal 16449. Then, bdfal 16449 can be proved from this theorem, using fal 1404. The total number of proof steps would be 17 (for bdnthALT 16451) + 3 = 20, which is more than 8 (for bdfal 16449) + 9 (for bdnth 16450) = 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 16448	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 16433	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 634	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	mptru 1406	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 708	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 16440	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1398  BOUNDED wbd 16428

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 16429  ax-bdim 16430  ax-bdn 16433  ax-bdeq 16436

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

This theorem is referenced by: (None)