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

Theorem bdnthALT 12438
 Description: Alternate proof of bdnth 12437 not using bdfal 12436. Then, bdfal 12436 can be proved from this theorem, using fal 1303. The total number of proof steps would be 17 (for bdnthALT 12438) + 3 = 20, which is more than 8 (for bdfal 12436) + 9 (for bdnth 12437) = 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 12435 . . 3 BOUNDED
21ax-bdn 12420 . 2 BOUNDED ¬ ⊤
3 notnot 597 . . . 4 (⊤ → ¬ ¬ ⊤)
43mptru 1305 . . 3 ¬ ¬ ⊤
5 bdnth.1 . . 3 ¬ 𝜑
64, 52false 655 . 2 (¬ ⊤ ↔ 𝜑)
72, 6bd0 12427 1 BOUNDED 𝜑
 Colors of variables: wff set class Syntax hints:  ¬ wn 3  ⊤wtru 1297  BOUNDED wbd 12415 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-bd0 12416  ax-bdim 12417  ax-bdn 12420  ax-bdeq 12423 This theorem depends on definitions:  df-bi 116  df-tru 1299 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator