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  2127  nexr  2192  nonconne  2952  ruOLD  3787  reu0  4361  neldifsn  4792  axnulALT  5304  nvel  5316  nfnid  5375  nprrel  5744  0xp  5784  son2lpi  6148  nlim0  6443  snsn0non  6509  onnev  6511  nfunv  6599  dffv3  6902  mpo0  7518  onprc  7798  ordeleqon  7802  onuninsuci  7861  orduninsuc  7864  iprc  7933  poxp2  8168  poxp3  8175  tfrlem13  8430  tfrlem14  8431  tfrlem16  8433  tfr2b  8436  tz7.44lem1  8445  nlim1  8527  nlim2  8528  sdomn2lp  9156  canth2  9170  map2xp  9187  snnen2o  9273  1sdom2dom  9283  fi0  9460  sucprcreg  9641  rankxplim3  9921  alephnbtwn2  10112  alephprc  10139  unialeph  10141  kmlem16  10206  cfsuc  10297  nd1  10627  nd2  10628  canthp1lem2  10693  0nnq  10964  1ne0sr  11136  pnfnre  11302  mnfnre  11304  ine0  11698  recgt0ii  12174  inelr  12256  0nnn  12302  nnunb  12522  nn0nepnf  12607  indstr  12958  1nuz2  12966  0nrp  13070  lsw0  14603  egt2lt3  16242  ruc  16279  odd2np1  16378  divalglem5  16434  bitsf1  16483  0nprm  16715  structcnvcnv  17190  fvsetsid  17205  fnpr2ob  17603  oduclatb  18552  0g0  18677  psgnunilem3  19514  zringndrg  21479  00ply1bas  22241  0ntop  22911  topnex  23003  bwth  23418  ustn0  24229  vitalilem5  25647  deg1nn0clb  26129  aaliou3lem9  26392  sinhalfpilem  26505  logdmn0  26682  dvlog  26693  ppiltx  27220  dchrisum0fno1  27555  nosgnn0i  27704  sltsolem1  27720  nolt02o  27740  nogt01o  27741  noprc  27824  oldirr  27928  leftirr  27929  rightirr  27930  axlowdim1  28974  topnfbey  30488  0ngrp  30530  dmadjrnb  31925  neldifpr1  32551  neldifpr2  32552  1nei  32747  nn0xmulclb  32775  ballotlem2  34491  bnj1304  34833  bnj110  34872  bnj98  34881  bnj1523  35085  subfacp1lem5  35189  msrrcl  35548  linedegen  36144  rankeq1o  36172  neufal  36407  neutru  36408  unqsym1  36426  onpsstopbas  36431  ordcmp  36448  onint1  36450  bj-ru  36945  bj-1nel0  36955  bj-0nelsngl  36972  bj-0nmoore  37113  bj-ccinftydisj  37214  relowlpssretop  37365  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem30  37657  zrdivrng  37960  prtlem400  38871  equidqe  38923  sn-inelr  42497  eldioph4b  42822  jm2.23  43008  ttac  43048  sucomisnotcard  43557  clsk1indlem1  44058  rusbcALT  44458  nimnbi  45168  nimnbi2  45169  fouriersw  46246  aibnbna  46918  dtrucor3  48719