Theorem bdnthALT 16775

Description: Alternate proof of bdnth 16774 not using bdfal 16773. Then, bdfal 16773 can be proved from this theorem, using fal 1409. The total number of proof steps would be 17 (for bdnthALT 16775) + 3 = 20, which is more than 8 (for bdfal 16773) + 9 (for bdnth 16774) = 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 16772	. . 3 ⊢ BOUNDED ⊤
2	1	ax-bdn 16757	. 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 16764	1 ⊢ BOUNDED 𝜑

Syntax hints:  ¬ wn 3  ⊤wtru 1403  BOUNDED wbd 16752

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 623  ax-in2 624  ax-bd0 16753  ax-bdim 16754  ax-bdn 16757  ax-bdeq 16760

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

This theorem is referenced by: (None)