| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > mto | GIF version | ||
| Description: The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
| Ref | Expression |
|---|---|
| mto.1 | ⊢ ¬ 𝜓 |
| mto.2 | ⊢ (𝜑 → 𝜓) |
| Ref | Expression |
|---|---|
| mto | ⊢ ¬ 𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mto.2 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | mto.1 | . . 3 ⊢ ¬ 𝜓 | |
| 3 | 2 | a1i 9 | . 2 ⊢ (𝜑 → ¬ 𝜓) |
| 4 | 1, 3 | pm2.65i 640 | 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 615 ax-in2 616 |
| This theorem is referenced by: mtbi 671 pm3.2ni 814 pm5.16 829 intnan 930 intnanr 931 equidqe 1554 nexr 1714 ru 2996 neldifsn 3762 nvel 4176 nlim0 4440 snnex 4494 onprc 4599 dtruex 4606 ordsoexmid 4609 nprrel 4719 0xp 4754 iprc 4946 son2lpi 5078 nfunv 5303 0fv 5611 canth 5896 acexmidlema 5934 acexmidlemb 5935 acexmidlemab 5937 mpo0 6014 php5dom 6959 fi0 7076 pw1ne1 7340 pw1ne3 7341 sucpw1nel3 7344 3nelsucpw1 7345 0nnq 7476 0npr 7595 1ne0sr 7878 pnfnre 8113 mnfnre 8114 ine0 8465 inelr 8656 nn0nepnf 9365 1nuz2 9726 0nrp 9810 inftonninf 10585 lsw0 11039 eirr 12061 odd2np1 12155 n2dvds1 12194 1nprm 12407 structcnvcnv 12819 fvsetsid 12837 fnpr2ob 13143 0g0 13179 0ntop 14450 topnex 14529 bj-nvel 15795 pwle2 15897 exmidsbthrlem 15923 trirec0xor 15946 |
| Copyright terms: Public domain | W3C validator |