Theorem bdnthALT 16430

Description: Alternate proof of bdnth 16429 not using bdfal 16428. Then, bdfal 16428 can be proved from this theorem, using fal 1404. The total number of proof steps would be 17 (for bdnthALT 16430) + 3 = 20, which is more than 8 (for bdfal 16428) + 9 (for bdnth 16429) = 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 16427	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 16412	. 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 16419	1 ⊢ BOUNDED 𝜑

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

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 16408  ax-bdim 16409  ax-bdn 16412  ax-bdeq 16415

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

This theorem is referenced by: (None)