MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mto Structured version   Visualization version   GIF version

Theorem mto 198
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.)
Hypotheses
Ref Expression
mto.1 ¬ 𝜓
mto.2 (𝜑𝜓)
Assertion
Ref Expression
mto ¬ 𝜑

Proof of Theorem mto
StepHypRef Expression
1 mto.2 . 2 (𝜑𝜓)
2 mto.1 . . 3 ¬ 𝜓
32a1i 11 . 2 (𝜑 → ¬ 𝜓)
41, 3pm2.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