Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bdnthALT Structured version   Unicode version

Theorem bdnthALT 9224
Description: Alternate proof of bdnth 9223 not using bdfal 9222. Then, bdfal 9222 can be proved from this theorem, using fal 1249. The total number of proof steps would be 17 (for bdnthALT 9224) + 3 = 20, which is more than 8 (for bdfal 9222) + 9 (for bdnth 9223) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
bdnth.1
Assertion
Ref Expression
bdnthALT BOUNDED

Proof of Theorem bdnthALT
StepHypRef Expression
1 bdtru 9221 . . 3 BOUNDED
21ax-bdn 9206 . 2 BOUNDED
3 notnot1 559 . . . 4
43trud 1251 . . 3
5 bdnth.1 . . 3
64, 52false 616 . 2
72, 6bd0 9213 1 BOUNDED
Colors of variables: wff set class
Syntax hints:   wn 3   wtru 1243  BOUNDED wbd 9201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-bd0 9202  ax-bdim 9203  ax-bdn 9206  ax-bdeq 9209
This theorem depends on definitions:  df-bi 110  df-tru 1245
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator