![]() |
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 567 | 1 ⊢ ¬ φ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 544 ax-in2 545 |
This theorem is referenced by: mtbi 594 pm3.2ni 725 pm5.16 736 intnan 837 intnanr 838 equidqe 1422 nexr 1579 ru 2757 sspssn 3042 neldifsn 3488 nvel 3880 nlim0 4097 snnex 4147 onprc 4230 dtruex 4237 ordsoexmid 4240 nprrel 4329 0xp 4363 iprc 4543 son2lpi 4664 nfunv 4876 0fv 5151 acexmidlema 5446 acexmidlemb 5447 acexmidlemab 5449 mpt20 5516 0nnq 6348 0npr 6466 1ne0sr 6694 pnfnre 6864 mnfnre 6865 ine0 7187 inelr 7368 1nuz2 8319 0nrp 8391 bj-nvel 9352 |
Copyright terms: Public domain | W3C validator |