Theorem bdnthALT 13204

Description: Alternate proof of bdnth 13203 not using bdfal 13202. Then, bdfal 13202 can be proved from this theorem, using fal 1339. The total number of proof steps would be 17 (for bdnthALT 13204) + 3 = 20, which is more than 8 (for bdfal 13202) + 9 (for bdnth 13203) = 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 13201	. . 3 |- BOUNDED T.
2	1	ax-bdn 13186	. 2 |- BOUNDED -. T.
3		notnot 619	. . . 4 |- ( T. -> -. -. T. )
4	3	mptru 1341	. . 3 |- -. -. T.
5		bdnth.1	. . 3 |- -. ph
6	4, 5	2false 691	. 2 |- ( -. T. <-> ph )
7	2, 6	bd0 13193	1 |- BOUNDED ph

Syntax hints:   -. wn 3   T. wtru 1333  BOUNDED wbd 13181

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 13182  ax-bdim 13183  ax-bdn 13186  ax-bdeq 13189

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

This theorem is referenced by: (None)