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 874 nexr 2181 nonconne 3028 ru 3770 noel 4295 reu0 4317 neldifsn 4719 axnulALT 5200 nvel 5212 nfnid 5268 nprrel 5605 0xp 5643 son2lpi 5982 nlim0 6243 snsn0non 6303 nfunv 6382 dffv3 6660 mpo0 7228 onprc 7487 ordeleqon 7491 onuninsuci 7543 orduninsuc 7546 iprc 7606 tfrlem13 8017 tfrlem14 8018 tfrlem16 8020 tfr2b 8023 tz7.44lem1 8032 sdomn2lp 8645 canth2 8659 map2xp 8676 fi0 8873 sucprcreg 9054 rankxplim3 9299 alephnbtwn2 9487 alephprc 9514 unialeph 9516 kmlem16 9580 cfsuc 9668 nd1 9998 nd2 9999 canthp1lem2 10064 0nnq 10335 1ne0sr 10507 pnfnre 10671 mnfnre 10673 ine0 11064 recgt0ii 11535 inelr 11617 0nnn 11662 nnunb 11882 nn0nepnf 11964 indstr 12305 1nuz2 12313 0nrp 12414 lsw0 13907 egt2lt3 15549 ruc 15586 odd2np1 15680 n2dvds1OLD 15708 divalglem5 15738 bitsf1 15785 0nprm 16012 structcnvcnv 16487 fvsetsid 16505 fnpr2ob 16821 oduclatb 17744 0g0 17864 psgnunilem3 18555 00ply1bas 20338 zringndrg 20567 0ntop 21443 topnex 21534 bwth 21948 ustn0 22758 vitalilem5 24142 deg1nn0clb 24613 aaliou3lem9 24868 sinhalfpilem 24978 logdmn0 25150 dvlog 25161 ppiltx 25682 dchrisum0fno1 26015 axlowdim1 26673 topnfbey 28176 0ngrp 28216 dmadjrnb 29611 neldifpr1 30221 neldifpr2 30222 1nei 30399 nn0xmulclb 30423 ballotlem2 31646 bnj521 31907 bnj1304 31991 bnj110 32030 bnj98 32039 bnj1523 32241 subfacp1lem5 32329 msrrcl 32688 nosgnn0i 33064 sltsolem1 33078 nolt02o 33097 noprc 33147 linedegen 33502 rankeq1o 33530 neufal 33652 neutru 33653 unqsym1 33671 amosym1 33672 onpsstopbas 33676 ordcmp 33693 onint1 33695 bj-ru0 34151 bj-ru 34153 bj-1nel0 34164 bj-0nelsngl 34181 bj-0nmoore 34299 bj-ccinftydisj 34388 bj-isrvec 34464 relowlpssretop 34528 poimirlem16 34790 poimirlem17 34791 poimirlem18 34792 poimirlem19 34793 poimirlem20 34794 poimirlem22 34796 poimirlem30 34804 zrdivrng 35114 prtlem400 35888 equidqe 35940 nsb 38982 eldioph4b 39288 jm2.23 39473 ttac 39513 clsk1indlem1 40275 rusbcALT 40651 fouriersw 42397 aibnbna 43023 |
Copyright terms: Public domain | W3C validator |