Theorem bdnthALT 13677

Description: Alternate proof of bdnth 13676 not using bdfal 13675. Then, bdfal 13675 can be proved from this theorem, using fal 1350. The total number of proof steps would be 17 (for bdnthALT 13677) + 3 = 20, which is more than 8 (for bdfal 13675) + 9 (for bdnth 13676) = 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 13674	. . 3 |- BOUNDED T.
2	1	ax-bdn 13659	. 2 |- BOUNDED -. T.
3		notnot 619	. . . 4 |- ( T. -> -. -. T. )
4	3	mptru 1352	. . 3 |- -. -. T.
5		bdnth.1	. . 3 |- -. ph
6	4, 5	2false 691	. 2 |- ( -. T. <-> ph )
7	2, 6	bd0 13666	1 |- BOUNDED ph

Syntax hints:   -. wn 3   T. wtru 1344  BOUNDED wbd 13654

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 13655  ax-bdim 13656  ax-bdn 13659  ax-bdeq 13662

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

This theorem is referenced by: (None)