![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtod | Unicode version |
Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Ref | Expression |
---|---|
mtod.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mtod.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mtod |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtod.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mtod.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | a1d 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | pm2.65d 585 |
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-in1 544 ax-in2 545 |
This theorem is referenced by: mtoi 589 mtand 590 mtbid 596 mtbird 597 po2nr 4037 po3nr 4038 sotricim 4051 elirr 4224 en2lp 4232 cauappcvgprlemladdru 6628 cauappcvgprlemladdrl 6629 caucvgprlemladdrl 6649 msqge0 7400 mulge0 7403 squeeze0 7651 elnn0z 8034 fznlem 8675 frec2uzf1od 8873 bj-nnen2lp 9414 |
Copyright terms: Public domain | W3C validator |