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

Theorem bdnthALT 7201
Description: Alternate proof of bdnth 7200 not using bdfal 7199. Then, bdfal 7199 can be proved from this theorem, using fal 1233. The total number of proof steps would be 17 (for bdnthALT 7201) + 3 = 20, which is more than 8 (for bdfal 7199) + 9 (for bdnth 7200) = 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 7198 . . 3 BOUNDED
21ax-bdn 7183 . 2 BOUNDED ¬ ⊤
3 notnot1 547 . . . 4 ( ⊤ → ¬ ¬ ⊤ )
43trud 1235 . . 3 ¬ ¬ ⊤
5 bdnth.1 . . 3 ¬ φ
64, 52false 604 . 2 (¬ ⊤ ↔ φ)
72, 6bd0 7190 1 BOUNDED φ
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wtru 1227  BOUNDED wbd 7178
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-bd0 7179  ax-bdim 7180  ax-bdn 7183  ax-bdeq 7186
This theorem depends on definitions:  df-bi 110  df-tru 1229
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator