Theorem bdnthALT 15733

Description: Alternate proof of bdnth 15732 not using bdfal 15731. Then, bdfal 15731 can be proved from this theorem, using fal 1379. The total number of proof steps would be 17 (for bdnthALT 15733) + 3 = 20, which is more than 8 (for bdfal 15731) + 9 (for bdnth 15732) = 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 15730	. . 3 |- BOUNDED T.
2	1	ax-bdn 15715	. 2 |- BOUNDED -. T.
3		notnot 630	. . . 4 |- ( T. -> -. -. T. )
4	3	mptru 1381	. . 3 |- -. -. T.
5		bdnth.1	. . 3 |- -. ph
6	4, 5	2false 702	. 2 |- ( -. T. <-> ph )
7	2, 6	bd0 15722	1 |- BOUNDED ph

Syntax hints:   -. wn 3   T. wtru 1373  BOUNDED wbd 15710

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 15711  ax-bdim 15712  ax-bdn 15715  ax-bdeq 15718

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

This theorem is referenced by: (None)