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  2130  nexr  2195  nonconne  2940  ruOLD  3735  reu0  4308  neldifsn  4741  axnulALT  5240  nvel  5252  nfnid  5311  nprrel  5673  0xp  5713  xp0  5714  son2lpi  6074  nlim0  6366  snsn0non  6432  onnev  6434  nfunv  6514  dffv3  6818  mpo0  7431  onprc  7711  ordeleqon  7715  onuninsuci  7770  orduninsuc  7773  iprc  7841  poxp2  8073  poxp3  8080  tfrlem13  8309  tfrlem14  8310  tfrlem16  8312  tfr2b  8315  tz7.44lem1  8324  nlim1  8404  nlim2  8405  sdomn2lp  9029  canth2  9043  map2xp  9060  snnen2o  9129  1sdom2dom  9138  fi0  9304  sucprcreg  9490  rankxplim3  9774  alephnbtwn2  9963  alephprc  9990  unialeph  9992  kmlem16  10057  cfsuc  10148  nd1  10478  nd2  10479  canthp1lem2  10544  0nnq  10815  1ne0sr  10987  pnfnre  11153  mnfnre  11155  ine0  11552  recgt0ii  12028  inelr  12115  0nnn  12161  nnunb  12377  nn0nepnf  12462  indstr  12814  1nuz2  12822  0nrp  12927  lsw0  14472  egt2lt3  16115  ruc  16152  odd2np1  16252  divalglem5  16308  bitsf1  16357  0nprm  16589  structcnvcnv  17064  fvsetsid  17079  fnpr2ob  17462  oduclatb  18413  0g0  18572  psgnunilem3  19408  zringndrg  21405  00ply1bas  22152  0ntop  22820  topnex  22911  bwth  23325  ustn0  24136  vitalilem5  25540  deg1nn0clb  26022  aaliou3lem9  26285  sinhalfpilem  26399  logdmn0  26576  dvlog  26587  ppiltx  27114  dchrisum0fno1  27449  nosgnn0i  27598  sltsolem1  27614  nolt02o  27634  nogt01o  27635  noprc  27719  oldirr  27835  leftirr  27836  rightirr  27837  axlowdim1  28937  topnfbey  30449  0ngrp  30491  dmadjrnb  31886  neldifpr1  32513  neldifpr2  32514  1nei  32720  nn0xmulclb  32754  cos9thpinconstr  33804  trisecnconstr  33805  ballotlem2  34502  bnj1304  34831  bnj110  34870  bnj98  34879  bnj1523  35083  subfacp1lem5  35228  msrrcl  35587  linedegen  36187  rankeq1o  36215  neufal  36450  neutru  36451  unqsym1  36469  onpsstopbas  36474  ordcmp  36491  onint1  36493  bj-ru  36988  bj-1nel0  36998  bj-0nelsngl  37015  bj-0nmoore  37156  bj-ccinftydisj  37257  relowlpssretop  37408  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem22  37692  poimirlem30  37700  zrdivrng  38003  prtlem400  38979  equidqe  39031  sn-inelr  42590  eldioph4b  42914  jm2.23  43099  ttac  43139  sucomisnotcard  43647  clsk1indlem1  44148  rusbcALT  44541  nimnbi  45270  nimnbi2  45271  fouriersw  46339  nthrucw  46994  cjnpoly  46999  tannpoly  47000  sinnpoly  47001  aibnbna  47016  dtrucor3  48909  fonex  48977