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

Theorem bdnthALT 9955
 Description: Alternate proof of bdnth 9954 not using bdfal 9953. Then, bdfal 9953 can be proved from this theorem, using fal 1250. The total number of proof steps would be 17 (for bdnthALT 9955) + 3 = 20, which is more than 8 (for bdfal 9953) + 9 (for bdnth 9954) = 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 9952 . . 3 BOUNDED
21ax-bdn 9937 . 2 BOUNDED
3 notnot 559 . . . 4
43trud 1252 . . 3
5 bdnth.1 . . 3
64, 52false 617 . 2
72, 6bd0 9944 1 BOUNDED
 Colors of variables: wff set class Syntax hints:   wn 3   wtru 1244  BOUNDED wbd 9932 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 9933  ax-bdim 9934  ax-bdn 9937  ax-bdeq 9940 This theorem depends on definitions:  df-bi 110  df-tru 1246 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator