![]() |
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 157. (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 195 | 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 202 mtbi 323 intnan 487 intnanr 488 pm3.2ni 875 nexr 2154 nonconne 2995 ru 3706 noel 4218 reu0 4240 neldifsn 4634 axnulALT 5102 nvel 5114 nfnid 5170 nprrel 5500 0xp 5538 son2lpi 5867 nlim0 6127 snsn0non 6187 nfunv 6261 dffv3 6537 mpo0 7098 onprc 7358 ordeleqon 7362 onuninsuci 7414 orduninsuc 7417 iprc 7477 tfrlem13 7881 tfrlem14 7882 tfrlem16 7884 tfr2b 7887 tz7.44lem1 7896 sdomn2lp 8506 canth2 8520 map2xp 8537 fi0 8733 sucprcreg 8914 rankxplim3 9159 alephnbtwn2 9347 alephprc 9374 unialeph 9376 kmlem16 9440 cfsuc 9528 nd1 9858 nd2 9859 canthp1lem2 9924 0nnq 10195 1ne0sr 10367 pnfnre 10531 mnfnre 10533 ine0 10925 recgt0ii 11396 inelr 11478 0nnn 11523 nnunb 11743 nn0nepnf 11825 indstr 12165 1nuz2 12173 0nrp 12274 lsw0 13763 egt2lt3 15392 ruc 15429 odd2np1 15523 n2dvds1OLD 15551 divalglem5 15581 bitsf1 15628 0nprm 15851 structcnvcnv 16326 fvsetsid 16344 fnpr2ob 16660 oduclatb 17583 0g0 17702 psgnunilem3 18355 00ply1bas 20091 zringndrg 20319 0ntop 21197 topnex 21288 bwth 21702 ustn0 22512 vitalilem5 23896 deg1nn0clb 24367 aaliou3lem9 24622 sinhalfpilem 24732 logdmn0 24904 dvlog 24915 ppiltx 25436 dchrisum0fno1 25769 axlowdim1 26428 topnfbey 27931 0ngrp 27971 dmadjrnb 29366 neldifpr1 29974 neldifpr2 29975 1nei 30152 nn0xmulclb 30176 ballotlem2 31355 bnj521 31616 bnj1304 31700 bnj110 31738 bnj98 31747 bnj1523 31949 subfacp1lem5 32033 msrrcl 32392 nosgnn0i 32769 sltsolem1 32783 nolt02o 32802 noprc 32852 linedegen 33207 rankeq1o 33235 neufal 33357 neutru 33358 unqsym1 33376 amosym1 33377 onpsstopbas 33381 ordcmp 33398 onint1 33400 bj-ru0 33822 bj-ru 33824 bj-1nel0 33835 bj-0nelsngl 33901 bj-0nmoore 34017 bj-ccinftydisj 34066 relowlpssretop 34189 poimirlem16 34452 poimirlem17 34453 poimirlem18 34454 poimirlem19 34455 poimirlem20 34456 poimirlem22 34458 poimirlem30 34466 zrdivrng 34776 prtlem400 35550 equidqe 35602 nsb 38644 eldioph4b 38906 jm2.23 39091 ttac 39131 clsk1indlem1 39893 rusbcALT 40322 fouriersw 42072 aibnbna 42697 |
Copyright terms: Public domain | W3C validator |