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

Theorem bdnthALT 12960
Description: Alternate proof of bdnth 12959 not using bdfal 12958. Then, bdfal 12958 can be proved from this theorem, using fal 1323. The total number of proof steps would be 17 (for bdnthALT 12960) + 3 = 20, which is more than 8 (for bdfal 12958) + 9 (for bdnth 12959) = 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 12957 . . 3  |- BOUNDED T.
21ax-bdn 12942 . 2  |- BOUNDED  -. T.
3 notnot 603 . . . 4  |-  ( T. 
->  -.  -. T.  )
43mptru 1325 . . 3  |-  -.  -. T.
5 bdnth.1 . . 3  |-  -.  ph
64, 52false 675 . 2  |-  ( -. T.  <->  ph )
72, 6bd0 12949 1  |- BOUNDED  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   T. wtru 1317  BOUNDED wbd 12937
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 588  ax-in2 589  ax-bd0 12938  ax-bdim 12939  ax-bdn 12942  ax-bdeq 12945
This theorem depends on definitions:  df-bi 116  df-tru 1319
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator