Theorem bdnthALT 17027

Description: Alternate proof of bdnth 17026 not using bdfal 17025. Then, bdfal 17025 can be proved from this theorem, using fal 1409. The total number of proof steps would be 17 (for bdnthALT 17027) + 3 = 20, which is more than 8 (for bdfal 17025) + 9 (for bdnth 17026) = 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 17024	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 17009	. 2 ⊢ BOUNDED ¬ ⊤
3		notnot 638	. . . 4 ⊢ (⊤ → ¬ ¬ ⊤)
4	3	mptru 1411	. . 3 ⊢ ¬ ¬ ⊤
5		bdnth.1	. . 3 ⊢ ¬ 𝜑
6	4, 5	2false 713	. 2 ⊢ (¬ ⊤ ↔ 𝜑)
7	2, 6	bd0 17016	1 ⊢ BOUNDED 𝜑

This proof depends on syntax axioms:  ¬ wn 3  ⊤wtru 1403  BOUNDED wbd 17004

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-bd0 17005  ax-bdim 17006  ax-bdn 17009  ax-bdeq 17012

This proof depends on definitions:  df-bi 117  df-tru 1405

This theorem is used by: (None)