![]() |
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 150. (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 185 | 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 192 mtbi 311 pm3.2ni 935 intnan 998 intnanr 999 nexr 2209 nonconne 2944 ru 3575 neldifsn 4467 axnulALT 4939 nvel 4949 nfnid 5046 nprrel 5318 0xp 5356 son2lpi 5682 nlim0 5944 snsn0non 6007 nfunv 6082 dffv3 6348 mpt20 6890 snnexOLD 7132 onprc 7149 ordeleqon 7153 onuninsuci 7205 orduninsuc 7208 iprc 7266 tfrlem13 7655 tfrlem14 7656 tfrlem16 7658 tfr2b 7661 tz7.44lem1 7670 sdomn2lp 8264 canth2 8278 map2xp 8295 fi0 8491 sucprcreg 8671 rankxplim3 8917 alephnbtwn2 9085 alephprc 9112 unialeph 9114 kmlem16 9179 cfsuc 9271 nd1 9601 nd2 9602 canthp1lem2 9667 0nnq 9938 1ne0sr 10109 pnfnre 10273 mnfnre 10274 ine0 10657 recgt0ii 11121 inelr 11202 nnunb 11480 nn0nepnf 11563 indstr 11949 1nuz2 11957 0nrp 12058 zgt1rpn0n1 12064 lsw0 13539 egt2lt3 15133 ruc 15171 odd2np1 15267 n2dvds1 15306 divalglem5 15322 bitsf1 15370 structcnvcnv 16073 fvsetsid 16092 strlemor1OLD 16171 meet0 17338 join0 17339 oduclatb 17345 0g0 17464 psgnunilem3 18116 00ply1bas 19812 zringndrg 20040 0ntop 20912 topnex 21002 bwth 21415 ustn0 22225 vitalilem5 23580 deg1nn0clb 24049 aaliou3lem9 24304 sinhalfpilem 24414 logdmn0 24585 dvlog 24596 ppiltx 25102 dchrisum0fno1 25399 axlowdim1 26038 topnfbey 27636 0ngrp 27674 dmadjrnb 29074 ballotlem2 30859 bnj521 31112 bnj1304 31197 bnj110 31235 bnj98 31244 bnj1523 31446 subfacp1lem5 31473 msrrcl 31747 nosgnn0i 32118 sltsolem1 32132 nolt02o 32151 noprc 32201 linedegen 32556 rankeq1o 32584 unnf 32712 unnt 32713 unqsym1 32730 amosym1 32731 onpsstopbas 32735 ordcmp 32752 onint1 32754 bj-babygodel 32894 bj-ru0 33238 bj-ru 33240 bj-1nel0 33247 bj-0nelsngl 33265 bj-0nmoore 33373 bj-ccinftydisj 33411 relowlpssretop 33523 poimirlem16 33738 poimirlem17 33739 poimirlem18 33740 poimirlem19 33741 poimirlem20 33742 poimirlem22 33744 poimirlem30 33752 zrdivrng 34065 prtlem400 34659 equidqe 34711 eldioph4b 37877 jm2.23 38065 ttac 38105 clsk1indlem1 38845 rusbcALT 39142 fouriersw 40951 aibnbna 41579 |
Copyright terms: Public domain | W3C validator |