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  880  ru0  2128  nexr  2193  nonconne  2937  ruOLD  3741  reu0  4312  neldifsn  4743  axnulALT  5243  nvel  5255  nfnid  5314  nprrel  5678  0xp  5718  son2lpi  6077  nlim0  6367  snsn0non  6433  onnev  6435  nfunv  6515  dffv3  6818  mpo0  7434  onprc  7714  ordeleqon  7718  onuninsuci  7773  orduninsuc  7776  iprc  7844  poxp2  8076  poxp3  8083  tfrlem13  8312  tfrlem14  8313  tfrlem16  8315  tfr2b  8318  tz7.44lem1  8327  nlim1  8407  nlim2  8408  sdomn2lp  9033  canth2  9047  map2xp  9064  snnen2o  9134  1sdom2dom  9143  fi0  9310  sucprcreg  9496  rankxplim3  9777  alephnbtwn2  9966  alephprc  9993  unialeph  9995  kmlem16  10060  cfsuc  10151  nd1  10481  nd2  10482  canthp1lem2  10547  0nnq  10818  1ne0sr  10990  pnfnre  11156  mnfnre  11158  ine0  11555  recgt0ii  12031  inelr  12118  0nnn  12164  nnunb  12380  nn0nepnf  12465  indstr  12817  1nuz2  12825  0nrp  12930  lsw0  14472  egt2lt3  16115  ruc  16152  odd2np1  16252  divalglem5  16308  bitsf1  16357  0nprm  16589  structcnvcnv  17064  fvsetsid  17079  fnpr2ob  17462  oduclatb  18413  0g0  18538  psgnunilem3  19375  zringndrg  21375  00ply1bas  22122  0ntop  22790  topnex  22881  bwth  23295  ustn0  24106  vitalilem5  25511  deg1nn0clb  25993  aaliou3lem9  26256  sinhalfpilem  26370  logdmn0  26547  dvlog  26558  ppiltx  27085  dchrisum0fno1  27420  nosgnn0i  27569  sltsolem1  27585  nolt02o  27605  nogt01o  27606  noprc  27690  oldirr  27804  leftirr  27805  rightirr  27806  axlowdim1  28904  topnfbey  30413  0ngrp  30455  dmadjrnb  31850  neldifpr1  32477  neldifpr2  32478  1nei  32680  nn0xmulclb  32714  cos9thpinconstr  33758  trisecnconstr  33759  ballotlem2  34457  bnj1304  34786  bnj110  34825  bnj98  34834  bnj1523  35038  subfacp1lem5  35157  msrrcl  35516  linedegen  36117  rankeq1o  36145  neufal  36380  neutru  36381  unqsym1  36399  onpsstopbas  36404  ordcmp  36421  onint1  36423  bj-ru  36918  bj-1nel0  36928  bj-0nelsngl  36945  bj-0nmoore  37086  bj-ccinftydisj  37187  relowlpssretop  37338  poimirlem16  37616  poimirlem17  37617  poimirlem18  37618  poimirlem19  37619  poimirlem20  37620  poimirlem22  37622  poimirlem30  37630  zrdivrng  37933  prtlem400  38849  equidqe  38901  sn-inelr  42460  eldioph4b  42784  jm2.23  42969  ttac  43009  sucomisnotcard  43517  clsk1indlem1  44018  rusbcALT  44412  nimnbi  45141  nimnbi2  45142  fouriersw  46212  cjnpoly  46873  tannpoly  46874  sinnpoly  46875  aibnbna  46890  dtrucor3  48783  fonex  48851