![]() |
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 622 |
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 580 ax-in2 581 |
This theorem is referenced by: mtoi 626 mtand 627 mtbid 633 mtbird 634 po2nr 4145 po3nr 4146 sotricim 4159 elirr 4370 ordn2lp 4374 en2lp 4383 tfr1onlemsucaccv 6120 tfrcllemsucaccv 6133 nndomo 6634 fnfi 6700 cauappcvgprlemladdru 7269 cauappcvgprlemladdrl 7270 caucvgprlemladdrl 7291 caucvgprprlemaddq 7321 msqge0 8147 mulge0 8150 squeeze0 8419 elnn0z 8817 fznlem 9509 frec2uzf1od 9867 facndiv 10201 isumrblem 10819 alzdvds 11187 fzm1ndvds 11189 fzo0dvdseq 11190 rpdvds 11413 nonsq 11517 bj-nnen2lp 12115 |
Copyright terms: Public domain | W3C validator |