![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtod | GIF 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 650 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 604 ax-in2 605 |
This theorem is referenced by: mtoi 654 mtand 655 mtbid 662 mtbird 663 pwntru 4130 po2nr 4239 po3nr 4240 sotricim 4253 elirr 4464 ordn2lp 4468 en2lp 4477 tfr1onlemsucaccv 6246 tfrcllemsucaccv 6259 nndomo 6766 fnfi 6833 difinfsnlem 6992 cauappcvgprlemladdru 7488 cauappcvgprlemladdrl 7489 caucvgprlemladdrl 7510 caucvgprprlemaddq 7540 msqge0 8402 mulge0 8405 squeeze0 8686 elnn0z 9091 fznlem 9852 frec2uzf1od 10210 facndiv 10517 sumrbdclem 11178 prodrbdclem 11372 alzdvds 11588 fzm1ndvds 11590 fzo0dvdseq 11591 rpdvds 11816 nonsq 11921 ennnfonelemim 11973 bldisj 12609 bj-nnen2lp 13323 pwtrufal 13365 refeq 13398 |
Copyright terms: Public domain | W3C validator |