Theorem mto 196

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.)

Hypotheses

Ref	Expression
mto.1	⊢ ¬ 𝜓
mto.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
mto	⊢ ¬ 𝜑

Proof of Theorem 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 ⊢ ¬ 𝜑

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  322  intnan  487  intnanr  488  pm3.2ni  878  nexr  2185  nonconne  2955  ru  3715  noelOLD  4265  reu0  4292  neldifsn  4725  axnulALT  5228  nvel  5240  nfnid  5298  nprrel  5646  0xp  5685  son2lpi  6033  nlim0  6324  snsn0non  6385  onnev  6387  nfunv  6467  dffv3  6770  mpo0  7360  onprc  7628  ordeleqon  7632  onuninsuci  7687  orduninsuc  7690  iprc  7760  tfrlem13  8221  tfrlem14  8222  tfrlem16  8224  tfr2b  8227  tz7.44lem1  8236  nlim1  8319  nlim2  8320  sdomn2lp  8903  canth2  8917  map2xp  8934  snnen2o  9026  fi0  9179  sucprcreg  9360  rankxplim3  9639  alephnbtwn2  9828  alephprc  9855  unialeph  9857  kmlem16  9921  cfsuc  10013  nd1  10343  nd2  10344  canthp1lem2  10409  0nnq  10680  1ne0sr  10852  pnfnre  11016  mnfnre  11018  ine0  11410  recgt0ii  11881  inelr  11963  0nnn  12009  nnunb  12229  nn0nepnf  12313  indstr  12656  1nuz2  12664  0nrp  12765  lsw0  14268  egt2lt3  15915  ruc  15952  odd2np1  16050  divalglem5  16106  bitsf1  16153  0nprm  16383  structcnvcnv  16854  fvsetsid  16869  fnpr2ob  17269  oduclatb  18225  0g0  18348  psgnunilem3  19104  zringndrg  20690  00ply1bas  21411  0ntop  22054  topnex  22146  bwth  22561  ustn0  23372  vitalilem5  24776  deg1nn0clb  25255  aaliou3lem9  25510  sinhalfpilem  25620  logdmn0  25795  dvlog  25806  ppiltx  26326  dchrisum0fno1  26659  axlowdim1  27327  topnfbey  28833  0ngrp  28873  dmadjrnb  30268  neldifpr1  30881  neldifpr2  30882  1nei  31071  nn0xmulclb  31094  ballotlem2  32455  bnj521  32716  bnj1304  32799  bnj110  32838  bnj98  32847  bnj1523  33051  subfacp1lem5  33146  msrrcl  33505  poxp2  33790  poxp3  33796  nosgnn0i  33862  sltsolem1  33878  nolt02o  33898  nogt01o  33899  noprc  33974  oldirr  34072  leftirr  34073  rightirr  34074  linedegen  34445  rankeq1o  34473  neufal  34595  neutru  34596  unqsym1  34614  amosym1  34615  onpsstopbas  34619  ordcmp  34636  onint1  34638  bj-ru0  35131  bj-ru  35133  bj-1nel0  35144  bj-0nelsngl  35161  bj-0nmoore  35283  bj-ccinftydisj  35384  relowlpssretop  35535  poimirlem16  35793  poimirlem17  35794  poimirlem18  35795  poimirlem19  35796  poimirlem20  35797  poimirlem22  35799  poimirlem30  35807  zrdivrng  36111  prtlem400  36884  equidqe  36936  sn-inelr  40435  eldioph4b  40633  jm2.23  40818  ttac  40858  sucomisnotcard  41151  clsk1indlem1  41655  rusbcALT  42057  fouriersw  43772  aibnbna  44401  dtrucor3  46144