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

Theorem bdnthALT 10893
 Description: Alternate proof of bdnth 10892 not using bdfal 10891. Then, bdfal 10891 can be proved from this theorem, using fal 1292. The total number of proof steps would be 17 (for bdnthALT 10893) + 3 = 20, which is more than 8 (for bdfal 10891) + 9 (for bdnth 10892) = 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 10890 . . 3 BOUNDED
21ax-bdn 10875 . 2 BOUNDED ¬ ⊤
3 notnot 592 . . . 4 (⊤ → ¬ ¬ ⊤)
43trud 1294 . . 3 ¬ ¬ ⊤
5 bdnth.1 . . 3 ¬ 𝜑
64, 52false 650 . 2 (¬ ⊤ ↔ 𝜑)
72, 6bd0 10882 1 BOUNDED 𝜑
 Colors of variables: wff set class Syntax hints:  ¬ wn 3  ⊤wtru 1286  BOUNDED wbd 10870 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 10871  ax-bdim 10872  ax-bdn 10875  ax-bdeq 10878 This theorem depends on definitions:  df-bi 115  df-tru 1288 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator