Theorem mto 196

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 193	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  200  mtbi  321  intnan  486  intnanr  487  pm3.2ni  877  nexr  2187  nonconne  2954  ru  3710  noelOLD  4262  reu0  4289  neldifsn  4722  axnulALT  5223  nvel  5235  nfnid  5293  nprrel  5637  0xp  5675  son2lpi  6022  nlim0  6309  snsn0non  6370  onnev  6372  nfunv  6451  dffv3  6752  mpo0  7338  onprc  7605  ordeleqon  7609  onuninsuci  7662  orduninsuc  7665  iprc  7734  tfrlem13  8192  tfrlem14  8193  tfrlem16  8195  tfr2b  8198  tz7.44lem1  8207  sdomn2lp  8852  canth2  8866  map2xp  8883  fi0  9109  sucprcreg  9290  rankxplim3  9570  alephnbtwn2  9759  alephprc  9786  unialeph  9788  kmlem16  9852  cfsuc  9944  nd1  10274  nd2  10275  canthp1lem2  10340  0nnq  10611  1ne0sr  10783  pnfnre  10947  mnfnre  10949  ine0  11340  recgt0ii  11811  inelr  11893  0nnn  11939  nnunb  12159  nn0nepnf  12243  indstr  12585  1nuz2  12593  0nrp  12694  lsw0  14196  egt2lt3  15843  ruc  15880  odd2np1  15978  divalglem5  16034  bitsf1  16081  0nprm  16311  structcnvcnv  16782  fvsetsid  16797  fnpr2ob  17186  oduclatb  18140  0g0  18263  psgnunilem3  19019  zringndrg  20602  00ply1bas  21321  0ntop  21962  topnex  22054  bwth  22469  ustn0  23280  vitalilem5  24681  deg1nn0clb  25160  aaliou3lem9  25415  sinhalfpilem  25525  logdmn0  25700  dvlog  25711  ppiltx  26231  dchrisum0fno1  26564  axlowdim1  27230  topnfbey  28734  0ngrp  28774  dmadjrnb  30169  neldifpr1  30782  neldifpr2  30783  1nei  30973  nn0xmulclb  30996  ballotlem2  32355  bnj521  32616  bnj1304  32699  bnj110  32738  bnj98  32747  bnj1523  32951  subfacp1lem5  33046  msrrcl  33405  poxp2  33717  poxp3  33723  nosgnn0i  33789  sltsolem1  33805  nolt02o  33825  nogt01o  33826  noprc  33901  oldirr  33999  leftirr  34000  rightirr  34001  linedegen  34372  rankeq1o  34400  neufal  34522  neutru  34523  unqsym1  34541  amosym1  34542  onpsstopbas  34546  ordcmp  34563  onint1  34565  bj-ru0  35058  bj-ru  35060  bj-1nel0  35071  bj-0nelsngl  35088  bj-0nmoore  35210  bj-ccinftydisj  35311  relowlpssretop  35462  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem30  35734  zrdivrng  36038  prtlem400  36811  equidqe  36863  sn-inelr  40356  eldioph4b  40549  jm2.23  40734  ttac  40774  clsk1indlem1  41544  rusbcALT  41946  fouriersw  43662  aibnbna  44288  dtrucor3  46032