Theorem mto 197

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 194	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  201  mtbi  322  intnan  486  intnanr  487  pm3.2ni  881  ru0  2133  nexr  2200  nonconne  2944  ruOLD  3727  reu0  4301  neldifsn  4737  axnulALT  5239  nvel  5254  nvelOLD  5257  nfnid  5317  nprrel  5690  0xp  5730  xp0  5731  son2lpi  6091  nlim0  6383  snsn0non  6449  onnev  6451  nfunv  6531  dffv3  6836  mpo0  7452  onprc  7732  ordeleqon  7736  onuninsuci  7791  orduninsuc  7794  iprc  7862  poxp2  8093  poxp3  8100  tfrlem13  8329  tfrlem14  8330  tfrlem16  8332  tfr2b  8335  tz7.44lem1  8344  nlim1  8424  nlim2  8425  sdomn2lp  9054  canth2  9068  map2xp  9085  ordfin  9150  snnen2o  9155  1sdom2dom  9164  fi0  9333  nelaneq  9516  sucprcregOLD  9521  rankxplim3  9805  alephnbtwn2  9994  alephprc  10021  unialeph  10023  kmlem16  10088  cfsuc  10179  nd1  10510  nd2  10511  canthp1lem2  10576  0nnq  10847  1ne0sr  11019  pnfnre  11186  mnfnre  11188  ine0  11585  recgt0ii  12062  inelr  12149  0nnn  12213  nnunb  12433  nn0nepnf  12518  indstr  12866  1nuz2  12874  0nrp  12979  lsw0  14527  egt2lt3  16173  ruc  16210  odd2np1  16310  divalglem5  16366  bitsf1  16415  0nprm  16647  structcnvcnv  17123  fvsetsid  17138  fnpr2ob  17522  oduclatb  18473  0g0  18632  psgnunilem3  19471  zringndrg  21448  00ply1bas  22203  0ntop  22870  topnex  22961  bwth  23375  ustn0  24186  vitalilem5  25579  deg1nn0clb  26055  aaliou3lem9  26316  sinhalfpilem  26427  logdmn0  26604  dvlog  26615  ppiltx  27140  dchrisum0fno1  27474  nosgnn0i  27623  ltssolem1  27639  nolt02o  27659  nogt01o  27660  noprc  27748  oldirr  27882  leftirr  27883  rightirr  27884  axlowdim1  29028  topnfbey  30539  0ngrp  30582  dmadjrnb  31977  neldifpr1  32603  neldifpr2  32604  1nei  32810  nn0xmulclb  32844  gsummulsubdishift1  33129  ply1coedeg  33649  cos9thpinconstr  33935  trisecnconstr  33936  ballotlem2  34633  bnj1304  34961  bnj110  35000  bnj98  35009  bnj1523  35213  axnulALT2  35224  fineqvinfep  35269  subfacp1lem5  35366  msrrcl  35725  linedegen  36325  rankeq1o  36353  neufal  36588  neutru  36589  unqsym1  36607  onpsstopbas  36612  ordcmp  36629  onint1  36631  elttcirr  36713  bj-ru  37251  bj-1nel0  37261  bj-0nelsngl  37278  bj-0nmoore  37424  bj-ccinftydisj  37527  relowlpssretop  37680  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem30  37971  zrdivrng  38274  prtlem400  39316  equidqe  39368  sn-inelr  42932  eldioph4b  43239  jm2.23  43424  ttac  43464  sucomisnotcard  43971  clsk1indlem1  44472  rusbcALT  44865  nimnbi  45593  nimnbi2  45594  fouriersw  46659  nthrucw  47316  cjnpoly  47337  tannpoly  47338  sinnpoly  47339  aibnbna  47354  dtrucor3  49274  fonex  49342