Theorem bdnthALT 15565

Description: Alternate proof of bdnth 15564 not using bdfal 15563. Then, bdfal 15563 can be proved from this theorem, using fal 1371. The total number of proof steps would be 17 (for bdnthALT 15565) + 3 = 20, which is more than 8 (for bdfal 15563) + 9 (for bdnth 15564) = 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 15562	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 15547	. 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 15554	1 ⊢ BOUNDED 𝜑

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

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 15543  ax-bdim 15544  ax-bdn 15547  ax-bdeq 15550

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

This theorem is referenced by: (None)