Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mto | Structured version Visualization version 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 mode that by denying denies" - remark in [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 5. Note that this rule is also valid in intuitionistic logic. Inference associated with con3i 149. (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 11 | . 2 ⊢ (𝜑 → ¬ 𝜓) |
4 | 1, 3 | pm2.65i 184 | 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 191 mtbi 311 pm3.2ni 895 intnan 951 intnanr 952 nexr 2050 nonconne 2794 ru 3401 neldifsn 4262 axnulALT 4715 nvel 4725 nfnid 4823 nprrel 5084 0xp 5122 son2lpi 5443 nlim0 5700 snsn0non 5763 nfunv 5835 dffv3 6099 mpt20 6623 snnex 6862 onprc 6876 ordeleqon 6880 onuninsuci 6932 orduninsuc 6935 iprc 6993 tfrlem13 7373 tfrlem14 7374 tfrlem16 7376 tfr2b 7379 tz7.44lem1 7388 sdomn2lp 7984 canth2 7998 map2xp 8015 fi0 8209 sucprcreg 8389 rankxplim3 8627 alephnbtwn2 8778 alephprc 8805 unialeph 8807 kmlem16 8870 cfsuc 8962 nd1 9288 nd2 9289 canthp1lem2 9354 0nnq 9625 1ne0sr 9796 pnfnre 9960 mnfnre 9961 ine0 10344 recgt0ii 10808 inelr 10887 nnunb 11165 nn0nepnf 11248 indstr 11632 1nuz2 11640 0nrp 11741 zgt1rpn0n1 11747 lsw0 13205 egt2lt3 14773 ruc 14811 odd2np1 14903 n2dvds1 14942 divalglem5 14958 bitsf1 15006 structcnvcnv 15706 fvsetsid 15722 strlemor1 15796 meet0 16960 join0 16961 oduclatb 16967 0g0 17086 psgnunilem3 17739 00ply1bas 19431 zringndrg 19657 0ntop 20535 bwth 21023 ustn0 21834 vitalilem5 23187 deg1nn0clb 23654 aaliou3lem9 23909 sinhalfpilem 24019 logdmn0 24186 dvlog 24197 ppiltx 24703 dchrisum0fno1 25000 axlowdim1 25639 wlkntrllem3 26091 spthispth 26103 topnfbey 26717 0ngrp 26749 dmadjrnb 28149 ballotlem2 29877 bnj521 30059 bnj1304 30144 bnj110 30182 bnj98 30191 bnj1523 30393 subfacp1lem5 30420 msrrcl 30694 nosgnn0i 31056 sltsolem1 31067 noprc 31080 linedegen 31420 rankeq1o 31448 unnf 31576 unnt 31577 unqsym1 31594 amosym1 31595 onpsstopbas 31599 ordcmp 31616 onint1 31618 bj-babygodel 31761 bj-ru0 32124 bj-ru 32126 bj-1nel0 32134 bj-0nelsngl 32152 bj-topnex 32247 bj-ccinftydisj 32277 relowlpssretop 32388 poimirlem16 32595 poimirlem17 32596 poimirlem18 32597 poimirlem19 32598 poimirlem20 32599 poimirlem22 32601 poimirlem30 32609 zrdivrng 32922 prtlem400 33173 equidqe 33225 eldioph4b 36393 jm2.23 36581 ttac 36621 clsk1indlem1 37363 rusbcALT 37662 fouriersw 39124 aibnbna 39722 |
Copyright terms: Public domain | W3C validator |