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  322  intnan  487  intnanr  488  pm3.2ni  878  nexr  2189  nonconne  2957  ru  3719  noelOLD  4271  reu0  4298  neldifsn  4731  axnulALT  5232  nvel  5244  nfnid  5302  nprrel  5647  0xp  5685  son2lpi  6032  nlim0  6323  snsn0non  6384  onnev  6386  nfunv  6465  dffv3  6767  mpo0  7354  onprc  7622  ordeleqon  7626  onuninsuci  7681  orduninsuc  7684  iprc  7754  tfrlem13  8212  tfrlem14  8213  tfrlem16  8215  tfr2b  8218  tz7.44lem1  8227  sdomn2lp  8885  canth2  8899  map2xp  8916  fi0  9157  sucprcreg  9338  rankxplim3  9640  alephnbtwn2  9829  alephprc  9856  unialeph  9858  kmlem16  9922  cfsuc  10014  nd1  10344  nd2  10345  canthp1lem2  10410  0nnq  10681  1ne0sr  10853  pnfnre  11017  mnfnre  11019  ine0  11410  recgt0ii  11881  inelr  11963  0nnn  12009  nnunb  12229  nn0nepnf  12313  indstr  12655  1nuz2  12663  0nrp  12764  lsw0  14266  egt2lt3  15913  ruc  15950  odd2np1  16048  divalglem5  16104  bitsf1  16151  0nprm  16381  structcnvcnv  16852  fvsetsid  16867  fnpr2ob  17267  oduclatb  18223  0g0  18346  psgnunilem3  19102  zringndrg  20688  00ply1bas  21409  0ntop  22052  topnex  22144  bwth  22559  ustn0  23370  vitalilem5  24774  deg1nn0clb  25253  aaliou3lem9  25508  sinhalfpilem  25618  logdmn0  25793  dvlog  25804  ppiltx  26324  dchrisum0fno1  26657  axlowdim1  27325  topnfbey  28829  0ngrp  28869  dmadjrnb  30264  neldifpr1  30877  neldifpr2  30878  1nei  31067  nn0xmulclb  31090  ballotlem2  32451  bnj521  32712  bnj1304  32795  bnj110  32834  bnj98  32843  bnj1523  33047  subfacp1lem5  33142  msrrcl  33501  poxp2  33786  poxp3  33792  nosgnn0i  33858  sltsolem1  33874  nolt02o  33894  nogt01o  33895  noprc  33970  oldirr  34068  leftirr  34069  rightirr  34070  linedegen  34441  rankeq1o  34469  neufal  34591  neutru  34592  unqsym1  34610  amosym1  34611  onpsstopbas  34615  ordcmp  34632  onint1  34634  bj-ru0  35127  bj-ru  35129  bj-1nel0  35140  bj-0nelsngl  35157  bj-0nmoore  35279  bj-ccinftydisj  35380  relowlpssretop  35531  poimirlem16  35789  poimirlem17  35790  poimirlem18  35791  poimirlem19  35792  poimirlem20  35793  poimirlem22  35795  poimirlem30  35803  zrdivrng  36107  prtlem400  36880  equidqe  36932  sn-inelr  40432  eldioph4b  40630  jm2.23  40815  ttac  40855  clsk1indlem1  41625  rusbcALT  42027  fouriersw  43743  aibnbna  44369  dtrucor3  46113