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

Theorem bdnthALT 13138
Description: Alternate proof of bdnth 13137 not using bdfal 13136. Then, bdfal 13136 can be proved from this theorem, using fal 1338. The total number of proof steps would be 17 (for bdnthALT 13138) + 3 = 20, which is more than 8 (for bdfal 13136) + 9 (for bdnth 13137) = 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 13135 . . 3 BOUNDED
21ax-bdn 13120 . 2 BOUNDED ¬ ⊤
3 notnot 618 . . . 4 (⊤ → ¬ ¬ ⊤)
43mptru 1340 . . 3 ¬ ¬ ⊤
5 bdnth.1 . . 3 ¬ 𝜑
64, 52false 690 . 2 (¬ ⊤ ↔ 𝜑)
72, 6bd0 13127 1 BOUNDED 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wtru 1332  BOUNDED wbd 13115
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 603  ax-in2 604  ax-bd0 13116  ax-bdim 13117  ax-bdn 13120  ax-bdeq 13123
This theorem depends on definitions:  df-bi 116  df-tru 1334
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator