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 3025 ru 3768 noel 4293 reu0 4315 neldifsn 4717 axnulALT 5199 nvel 5211 nfnid 5267 nprrel 5604 0xp 5642 son2lpi 5981 nlim0 6242 snsn0non 6302 nfunv 6381 dffv3 6659 mpo0 7228 onprc 7488 ordeleqon 7492 onuninsuci 7544 orduninsuc 7547 iprc 7607 tfrlem13 8015 tfrlem14 8016 tfrlem16 8018 tfr2b 8021 tz7.44lem1 8030 sdomn2lp 8644 canth2 8658 map2xp 8675 fi0 8872 sucprcreg 9053 rankxplim3 9298 alephnbtwn2 9486 alephprc 9513 unialeph 9515 kmlem16 9579 cfsuc 9667 nd1 9997 nd2 9998 canthp1lem2 10063 0nnq 10334 1ne0sr 10506 pnfnre 10670 mnfnre 10672 ine0 11063 recgt0ii 11534 inelr 11616 0nnn 11661 nnunb 11881 nn0nepnf 11963 indstr 12304 1nuz2 12312 0nrp 12412 lsw0 13905 egt2lt3 15547 ruc 15584 odd2np1 15678 n2dvds1OLD 15706 divalglem5 15736 bitsf1 15783 0nprm 16010 structcnvcnv 16485 fvsetsid 16503 fnpr2ob 16819 oduclatb 17742 0g0 17862 psgnunilem3 18553 00ply1bas 20336 zringndrg 20565 0ntop 21441 topnex 21532 bwth 21946 ustn0 22756 vitalilem5 24140 deg1nn0clb 24611 aaliou3lem9 24866 sinhalfpilem 24976 logdmn0 25150 dvlog 25161 ppiltx 25681 dchrisum0fno1 26014 axlowdim1 26672 topnfbey 28175 0ngrp 28215 dmadjrnb 29610 neldifpr1 30220 neldifpr2 30221 1nei 30398 nn0xmulclb 30422 ballotlem2 31645 bnj521 31906 bnj1304 31990 bnj110 32029 bnj98 32038 bnj1523 32240 subfacp1lem5 32328 msrrcl 32687 nosgnn0i 33063 sltsolem1 33077 nolt02o 33096 noprc 33146 linedegen 33501 rankeq1o 33529 neufal 33651 neutru 33652 unqsym1 33670 amosym1 33671 onpsstopbas 33675 ordcmp 33692 onint1 33694 bj-ru0 34150 bj-ru 34152 bj-1nel0 34163 bj-0nelsngl 34180 bj-0nmoore 34298 bj-ccinftydisj 34387 bj-isrvec 34463 relowlpssretop 34527 poimirlem16 34789 poimirlem17 34790 poimirlem18 34791 poimirlem19 34792 poimirlem20 34793 poimirlem22 34795 poimirlem30 34803 zrdivrng 35112 prtlem400 35886 equidqe 35938 nsb 38980 eldioph4b 39286 jm2.23 39471 ttac 39511 clsk1indlem1 40273 rusbcALT 40648 fouriersw 42393 aibnbna 43019 |
Copyright terms: Public domain | W3C validator |