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

Theorem bdnthALT 11069
Description: Alternate proof of bdnth 11068 not using bdfal 11067. Then, bdfal 11067 can be proved from this theorem, using fal 1292. The total number of proof steps would be 17 (for bdnthALT 11069) + 3 = 20, which is more than 8 (for bdfal 11067) + 9 (for bdnth 11068) = 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
StepHypRef Expression
1 bdtru 11066 . . 3  |- BOUNDED T.
21ax-bdn 11051 . 2  |- BOUNDED  -. T.
3 notnot 592 . . . 4  |-  ( T. 
->  -.  -. T.  )
43trud 1294 . . 3  |-  -.  -. T.
5 bdnth.1 . . 3  |-  -.  ph
64, 52false 650 . 2  |-  ( -. T.  <->  ph )
72, 6bd0 11058 1  |- BOUNDED  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   T. wtru 1286  BOUNDED wbd 11046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-bd0 11047  ax-bdim 11048  ax-bdn 11051  ax-bdeq 11054
This theorem depends on definitions:  df-bi 115  df-tru 1288
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator