Theorem bdnthALT 10626

Description: Alternate proof of bdnth 10625 not using bdfal 10624. Then, bdfal 10624 can be proved from this theorem, using fal 1291. The total number of proof steps would be 17 (for bdnthALT 10626) + 3 = 20, which is more than 8 (for bdfal 10624) + 9 (for bdnth 10625) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
bdnth.1	|- -. ph

Assertion

Ref	Expression
bdnthALT	|- BOUNDED ph

Proof of Theorem bdnthALT

Step	Hyp	Ref	Expression
1		bdtru 10623	. . 3 |- BOUNDED T.
2	1	ax-bdn 10608	. 2 |- BOUNDED -. T.
3		notnot 591	. . . 4 |- ( T. -> -. -. T. )
4	3	trud 1293	. . 3 |- -. -. T.
5		bdnth.1	. . 3 |- -. ph
6	4, 5	2false 649	. 2 |- ( -. T. <-> ph )
7	2, 6	bd0 10615	1 |- BOUNDED ph

Syntax hints:   -. wn 3   T. wtru 1285  BOUNDED wbd 10603

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-bd0 10604  ax-bdim 10605  ax-bdn 10608  ax-bdeq 10611

This theorem depends on definitions:  df-bi 115  df-tru 1287

This theorem is referenced by: (None)