![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > bdnthALT | Unicode version |
Description: Alternate proof of bdnth 14556 not using bdfal 14555. Then, bdfal 14555 can be proved from this theorem, using fal 1360. The total number of proof steps would be 17 (for bdnthALT 14557) + 3 = 20, which is more than 8 (for bdfal 14555) + 9 (for bdnth 14556) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bdnth.1 |
![]() ![]() ![]() |
Ref | Expression |
---|---|
bdnthALT |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bdtru 14554 |
. . 3
![]() ![]() | |
2 | 1 | ax-bdn 14539 |
. 2
![]() ![]() ![]() |
3 | notnot 629 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | mptru 1362 |
. . 3
![]() ![]() ![]() ![]() |
5 | bdnth.1 |
. . 3
![]() ![]() ![]() | |
6 | 4, 5 | 2false 701 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 6 | bd0 14546 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 14535 ax-bdim 14536 ax-bdn 14539 ax-bdeq 14542 |
This theorem depends on definitions: df-bi 117 df-tru 1356 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |