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 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 195	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  202  mtbi  323  intnan  487  intnanr  488  pm3.2ni  886  ru0  2138  nexr  2204  nonconne  2946  ruOLD  3722  reu0  4289  neldifsn  4725  axnulALT  5226  nvel  5241  nvelOLD  5244  nfnid  5304  nprrel  5677  0xp  5717  xp0  5718  son2lpi  6078  nlim0  6370  snsn0non  6436  onnev  6438  nfunv  6518  dffv3  6823  mpo0  7441  onprc  7721  ordeleqon  7725  onuninsuci  7780  orduninsuc  7783  iprc  7851  poxp2  8083  poxp3  8090  tfrlem13  8319  tfrlem14  8320  tfrlem16  8322  tfr2b  8325  tz7.44lem1  8334  nlim1  8414  nlim2  8415  sdomn2lp  9044  canth2  9058  map2xp  9075  ordfin  9140  snnen2o  9145  1sdom2dom  9154  fi0  9323  nelaneq  9507  sucprcregOLD  9512  rankxplim3  9796  alephnbtwn2  9985  alephprc  10012  unialeph  10014  kmlem16  10079  cfsuc  10170  nd1  10501  nd2  10502  canthp1lem2  10567  0nnq  10838  1ne0sr  11010  pnfnre  11177  mnfnre  11179  ine0  11576  recgt0ii  12053  inelr  12140  0nnn  12204  nnunb  12424  nn0nepnf  12509  indstr  12857  1nuz2  12865  0nrp  12970  lsw0  14518  egt2lt3  16164  ruc  16201  odd2np1  16301  divalglem5  16357  bitsf1  16406  0nprm  16638  structcnvcnv  17114  fvsetsid  17129  fnpr2ob  17513  oduclatb  18464  0g0  18623  psgnunilem3  19462  zringndrg  21443  00ply1bas  22224  0ntop  22888  topnex  22979  bwth  23393  ustn0  24204  vitalilem5  25597  deg1nn0clb  26073  aaliou3lem9  26334  sinhalfpilem  26445  logdmn0  26622  dvlog  26633  ppiltx  27158  dchrisum0fno1  27492  nosgnn0i  27641  ltssolem1  27657  nolt02o  27677  nogt01o  27678  noprc  27766  oldirr  27900  leftirr  27901  rightirr  27902  axlowdim1  29046  topnfbey  30557  0ngrp  30600  dmadjrnb  31995  neldifpr1  32621  neldifpr2  32622  1nei  32829  nn0xmulclb  32863  gsummulsubdishift1  33149  ply1coedeg  33672  cos9thpinconstr  33975  trisecnconstr  33976  ballotlem2  34673  bnj1304  35001  bnj110  35040  bnj98  35049  bnj1523  35253  axnulALT2  35264  fineqvinfep  35306  subfacp1lem5  35412  msrrcl  35771  linedegen  36371  rankeq1o  36399  neufal  36634  neutru  36635  unqsym1  36653  onpsstopbas  36658  ordcmp  36675  onint1  36677  elttcirr  36759  bj-ru  37297  bj-1nel0  37307  bj-0nelsngl  37324  bj-0nmoore  37470  bj-ccinftydisj  37573  relowlpssretop  37726  poimirlem16  38003  poimirlem17  38004  poimirlem18  38005  poimirlem19  38006  poimirlem20  38007  poimirlem22  38009  poimirlem30  38017  zrdivrng  38320  prtlem400  39362  equidqe  39414  sn-inelr  42977  eldioph4b  43256  jm2.23  43441  ttac  43481  sucomisnotcard  43988  clsk1indlem1  44489  rusbcALT  44882  nimnbi  45610  nimnbi2  45611  fouriersw  46674  nthrucw  47331  cjnpoly  47352  tannpoly  47353  sinnpoly  47354  aibnbna  47369  dtrucor3  49289  fonex  49357