Theorem mto 200

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 157. (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 197	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  204  mtbi  325  intnan  490  intnanr  491  pm3.2ni  881  nexr  2191  nonconne  2944  ru  3682  noelOLD  4232  reu0  4259  neldifsn  4691  axnulALT  5182  nvel  5194  nfnid  5253  nprrel  5593  0xp  5631  son2lpi  5973  nlim0  6249  snsn0non  6310  onnev  6312  nfunv  6391  dffv3  6691  mpo0  7274  onprc  7540  ordeleqon  7544  onuninsuci  7597  orduninsuc  7600  iprc  7669  tfrlem13  8104  tfrlem14  8105  tfrlem16  8107  tfr2b  8110  tz7.44lem1  8119  sdomn2lp  8763  canth2  8777  map2xp  8794  fi0  9014  sucprcreg  9195  rankxplim3  9462  alephnbtwn2  9651  alephprc  9678  unialeph  9680  kmlem16  9744  cfsuc  9836  nd1  10166  nd2  10167  canthp1lem2  10232  0nnq  10503  1ne0sr  10675  pnfnre  10839  mnfnre  10841  ine0  11232  recgt0ii  11703  inelr  11785  0nnn  11831  nnunb  12051  nn0nepnf  12135  indstr  12477  1nuz2  12485  0nrp  12586  lsw0  14085  egt2lt3  15730  ruc  15767  odd2np1  15865  divalglem5  15921  bitsf1  15968  0nprm  16198  structcnvcnv  16680  fvsetsid  16697  fnpr2ob  17017  oduclatb  17967  0g0  18090  psgnunilem3  18842  zringndrg  20409  00ply1bas  21115  0ntop  21756  topnex  21847  bwth  22261  ustn0  23072  vitalilem5  24463  deg1nn0clb  24942  aaliou3lem9  25197  sinhalfpilem  25307  logdmn0  25482  dvlog  25493  ppiltx  26013  dchrisum0fno1  26346  axlowdim1  27004  topnfbey  28506  0ngrp  28546  dmadjrnb  29941  neldifpr1  30554  neldifpr2  30555  1nei  30745  nn0xmulclb  30768  ballotlem2  32121  bnj521  32382  bnj1304  32466  bnj110  32505  bnj98  32514  bnj1523  32718  subfacp1lem5  32813  msrrcl  33172  poxp2  33470  poxp3  33476  nosgnn0i  33548  sltsolem1  33564  nolt02o  33584  nogt01o  33585  noprc  33660  oldirr  33758  leftirr  33759  rightirr  33760  linedegen  34131  rankeq1o  34159  neufal  34281  neutru  34282  unqsym1  34300  amosym1  34301  onpsstopbas  34305  ordcmp  34322  onint1  34324  bj-ru0  34817  bj-ru  34819  bj-1nel0  34830  bj-0nelsngl  34847  bj-0nmoore  34967  bj-ccinftydisj  35068  bj-isrvec  35148  relowlpssretop  35221  poimirlem16  35479  poimirlem17  35480  poimirlem18  35481  poimirlem19  35482  poimirlem20  35483  poimirlem22  35485  poimirlem30  35493  zrdivrng  35797  prtlem400  36570  equidqe  36622  sn-inelr  40084  eldioph4b  40277  jm2.23  40462  ttac  40502  clsk1indlem1  41273  rusbcALT  41671  fouriersw  43390  aibnbna  44016  dtrucor3  45760