![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtbird | Unicode version |
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.) |
Ref | Expression |
---|---|
mtbird.min |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mtbird.maj |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mtbird |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbird.min |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mtbird.maj |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimpd 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mtod 588 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-in1 544 ax-in2 545 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: eqneltrd 2130 neleqtrrd 2133 addnidpig 6320 nqnq0pi 6421 ltpopr 6569 cauappcvgprlemladdru 6628 caucvgprlemladdrl 6649 ltposr 6691 axltirr 6883 reapirr 7361 apirr 7389 indstr2 8322 xrltnsym 8484 xrlttr 8486 xrltso 8487 lbioog 8552 ubioog 8553 fzn 8676 expival 8911 |
Copyright terms: Public domain | W3C validator |