Theorem bdnthALT 13421

Description: Alternate proof of bdnth 13420 not using bdfal 13419. Then, bdfal 13419 can be proved from this theorem, using fal 1342. The total number of proof steps would be 17 (for bdnthALT 13421) + 3 = 20, which is more than 8 (for bdfal 13419) + 9 (for bdnth 13420) = 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 13418	. . 3 |- BOUNDED T.
2	1	ax-bdn 13403	. 2 |- BOUNDED -. T.
3		notnot 619	. . . 4 |- ( T. -> -. -. T. )
4	3	mptru 1344	. . 3 |- -. -. T.
5		bdnth.1	. . 3 |- -. ph
6	4, 5	2false 691	. 2 |- ( -. T. <-> ph )
7	2, 6	bd0 13410	1 |- BOUNDED ph

Syntax hints:   -. wn 3   T. wtru 1336  BOUNDED wbd 13398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-bd0 13399  ax-bdim 13400  ax-bdn 13403  ax-bdeq 13406

This theorem depends on definitions:  df-bi 116  df-tru 1338

This theorem is referenced by: (None)