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

Theorem bdnthALT 15775
Description: Alternate proof of bdnth 15774 not using bdfal 15773. Then, bdfal 15773 can be proved from this theorem, using fal 1380. The total number of proof steps would be 17 (for bdnthALT 15775) + 3 = 20, which is more than 8 (for bdfal 15773) + 9 (for bdnth 15774) = 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 15772 . . 3  |- BOUNDED T.
21ax-bdn 15757 . 2  |- BOUNDED  -. T.
3 notnot 630 . . . 4  |-  ( T. 
->  -.  -. T.  )
43mptru 1382 . . 3  |-  -.  -. T.
5 bdnth.1 . . 3  |-  -.  ph
64, 52false 703 . 2  |-  ( -. T.  <->  ph )
72, 6bd0 15764 1  |- BOUNDED  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   T. wtru 1374  BOUNDED wbd 15752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-bd0 15753  ax-bdim 15754  ax-bdn 15757  ax-bdeq 15760
This theorem depends on definitions:  df-bi 117  df-tru 1376
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator