![]() |
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 154. (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 193 | 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 200 mtbi 321 intnan 485 intnanr 486 pm3.2ni 878 nexr 2180 nonconne 2941 ru 3772 noelOLD 4331 reu0 4358 neldifsn 4797 axnulALT 5305 nvel 5317 nfnid 5375 nprrel 5737 0xp 5776 son2lpi 6135 nlim0 6430 snsn0non 6496 onnev 6498 nfunv 6587 dffv3 6892 mpo0 7505 onprc 7781 ordeleqon 7785 onuninsuci 7845 orduninsuc 7848 iprc 7919 poxp2 8148 poxp3 8155 tfrlem13 8411 tfrlem14 8412 tfrlem16 8414 tfr2b 8417 tz7.44lem1 8426 nlim1 8510 nlim2 8511 sdomn2lp 9141 canth2 9155 map2xp 9172 snnen2o 9262 1sdom2dom 9272 fi0 9445 sucprcreg 9626 rankxplim3 9906 alephnbtwn2 10097 alephprc 10124 unialeph 10126 kmlem16 10190 cfsuc 10282 nd1 10612 nd2 10613 canthp1lem2 10678 0nnq 10949 1ne0sr 11121 pnfnre 11287 mnfnre 11289 ine0 11681 recgt0ii 12153 inelr 12235 0nnn 12281 nnunb 12501 nn0nepnf 12585 indstr 12933 1nuz2 12941 0nrp 13044 lsw0 14551 egt2lt3 16186 ruc 16223 odd2np1 16321 divalglem5 16377 bitsf1 16424 0nprm 16652 structcnvcnv 17125 fvsetsid 17140 fnpr2ob 17543 oduclatb 18502 0g0 18627 psgnunilem3 19463 zringndrg 21411 00ply1bas 22182 0ntop 22851 topnex 22943 bwth 23358 ustn0 24169 vitalilem5 25585 deg1nn0clb 26070 aaliou3lem9 26330 sinhalfpilem 26443 logdmn0 26619 dvlog 26630 ppiltx 27154 dchrisum0fno1 27489 nosgnn0i 27638 sltsolem1 27654 nolt02o 27674 nogt01o 27675 noprc 27758 oldirr 27862 leftirr 27863 rightirr 27864 axlowdim1 28842 topnfbey 30351 0ngrp 30393 dmadjrnb 31788 neldifpr1 32408 neldifpr2 32409 1nei 32600 nn0xmulclb 32623 ballotlem2 34239 bnj1304 34581 bnj110 34620 bnj98 34629 bnj1523 34833 subfacp1lem5 34925 msrrcl 35284 linedegen 35870 rankeq1o 35898 neufal 36021 neutru 36022 unqsym1 36040 onpsstopbas 36045 ordcmp 36062 onint1 36064 bj-ru0 36552 bj-ru 36554 bj-1nel0 36564 bj-0nelsngl 36581 bj-0nmoore 36722 bj-ccinftydisj 36823 relowlpssretop 36974 poimirlem16 37240 poimirlem17 37241 poimirlem18 37242 poimirlem19 37243 poimirlem20 37244 poimirlem22 37246 poimirlem30 37254 zrdivrng 37557 prtlem400 38472 equidqe 38524 sn-inelr 42155 eldioph4b 42373 jm2.23 42559 ttac 42599 sucomisnotcard 43116 clsk1indlem1 43617 rusbcALT 44018 nimnbi 44674 nimnbi2 44675 fouriersw 45757 aibnbna 46426 dtrucor3 48057 |
Copyright terms: Public domain | W3C validator |