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 634 | 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 588 ax-in2 589 |
This theorem is referenced by: mtoi 638 mtand 639 mtbid 646 mtbird 647 pwntru 4092 po2nr 4201 po3nr 4202 sotricim 4215 elirr 4426 ordn2lp 4430 en2lp 4439 tfr1onlemsucaccv 6206 tfrcllemsucaccv 6219 nndomo 6726 fnfi 6793 difinfsnlem 6952 cauappcvgprlemladdru 7432 cauappcvgprlemladdrl 7433 caucvgprlemladdrl 7454 caucvgprprlemaddq 7484 msqge0 8346 mulge0 8349 squeeze0 8630 elnn0z 9035 fznlem 9789 frec2uzf1od 10147 facndiv 10453 sumrbdclem 11113 alzdvds 11479 fzm1ndvds 11481 fzo0dvdseq 11482 rpdvds 11707 nonsq 11812 ennnfonelemim 11864 bldisj 12497 bj-nnen2lp 13079 pwtrufal 13119 refeq 13150 |
Copyright terms: Public domain | W3C validator |