![]() |
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 661 |
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-in1 615 ax-in2 616 |
This theorem is referenced by: mtoi 665 mtand 666 mtbid 673 mtbird 674 pwntru 4211 po2nr 4321 po3nr 4322 sotricim 4335 elirr 4552 ordn2lp 4556 en2lp 4565 tfr1onlemsucaccv 6356 tfrcllemsucaccv 6369 nndomo 6878 fnfi 6950 difinfsnlem 7112 nninfwlpoimlemginf 7188 2omotaplemap 7270 cauappcvgprlemladdru 7669 cauappcvgprlemladdrl 7670 caucvgprlemladdrl 7691 caucvgprprlemaddq 7721 msqge0 8587 mulge0 8590 squeeze0 8875 elnn0z 9280 fznlem 10055 frec2uzf1od 10420 facndiv 10733 sumrbdclem 11399 prodrbdclem 11593 alzdvds 11874 fzm1ndvds 11876 fzo0dvdseq 11877 rpdvds 12113 nonsq 12221 prmdiv 12249 odzdvds 12259 pcprendvds 12304 pcprendvds2 12305 pcpremul 12307 pcdvdsb 12333 pockthlem 12368 1arith 12379 ennnfonelemim 12439 bldisj 14254 lgsdilem2 14790 lgsne0 14792 lgseisenlem1 14803 lgseisenlem2 14804 bj-nnen2lp 15059 pwtrufal 15101 refeq 15130 |
Copyright terms: Public domain | W3C validator |