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

Theorem bdnthALT 13677
Description: Alternate proof of bdnth 13676 not using bdfal 13675. Then, bdfal 13675 can be proved from this theorem, using fal 1350. The total number of proof steps would be 17 (for bdnthALT 13677) + 3 = 20, which is more than 8 (for bdfal 13675) + 9 (for bdnth 13676) = 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 13674 . . 3 BOUNDED
21ax-bdn 13659 . 2 BOUNDED ¬ ⊤
3 notnot 619 . . . 4 (⊤ → ¬ ¬ ⊤)
43mptru 1352 . . 3 ¬ ¬ ⊤
5 bdnth.1 . . 3 ¬ 𝜑
64, 52false 691 . 2 (¬ ⊤ ↔ 𝜑)
72, 6bd0 13666 1 BOUNDED 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wtru 1344  BOUNDED wbd 13654
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 604  ax-in2 605  ax-bd0 13655  ax-bdim 13656  ax-bdn 13659  ax-bdeq 13662
This theorem depends on definitions:  df-bi 116  df-tru 1346
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator