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

Theorem bdnthALT 14507
Description: Alternate proof of bdnth 14506 not using bdfal 14505. Then, bdfal 14505 can be proved from this theorem, using fal 1360. The total number of proof steps would be 17 (for bdnthALT 14507) + 3 = 20, which is more than 8 (for bdfal 14505) + 9 (for bdnth 14506) = 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 14504 . . 3 BOUNDED
21ax-bdn 14489 . 2 BOUNDED ¬ ⊤
3 notnot 629 . . . 4 (⊤ → ¬ ¬ ⊤)
43mptru 1362 . . 3 ¬ ¬ ⊤
5 bdnth.1 . . 3 ¬ 𝜑
64, 52false 701 . 2 (¬ ⊤ ↔ 𝜑)
72, 6bd0 14496 1 BOUNDED 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wtru 1354  BOUNDED wbd 14484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-bd0 14485  ax-bdim 14486  ax-bdn 14489  ax-bdeq 14492
This theorem depends on definitions:  df-bi 117  df-tru 1356
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator