New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mto | GIF version |
Description: The rule of modus tollens. The rule says, "if ψ is not true, and φ implies ψ, then ψ must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 5. (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 10 | . 2 ⊢ (φ → ¬ ψ) |
4 | 1, 3 | pm2.65i 165 | 1 ⊢ ¬ φ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: mt3 171 mtbi 289 pm3.2ni 827 intnan 880 intnanr 881 equidOLD 1677 nexr 1760 equidqe 2173 ru 3046 neldifsn 3842 0cnsuc 4402 vinf 4556 0cnelphi 4598 proj1op 4601 proj2op 4602 xp0r 4843 xpnedisj 5514 epprc 5828 nenpw1pwlem2 6086 2p1e3c 6157 ncvsq 6257 0lt1c 6259 nchoice 6309 vncan 6338 |
Copyright terms: Public domain | W3C validator |