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  488  intnanr  489  pm3.2ni  880  nexr  2186  nonconne  2953  ru  3775  noelOLD  4330  reu0  4357  neldifsn  4794  axnulALT  5303  nvel  5315  nfnid  5372  nprrel  5733  0xp  5772  son2lpi  6126  nlim0  6420  snsn0non  6486  onnev  6488  nfunv  6578  dffv3  6884  mpo0  7489  onprc  7760  ordeleqon  7764  onuninsuci  7824  orduninsuc  7827  iprc  7899  poxp2  8124  poxp3  8131  tfrlem13  8385  tfrlem14  8386  tfrlem16  8388  tfr2b  8391  tz7.44lem1  8400  nlim1  8484  nlim2  8485  sdomn2lp  9112  canth2  9126  map2xp  9143  snnen2o  9233  1sdom2dom  9243  fi0  9411  sucprcreg  9592  rankxplim3  9872  alephnbtwn2  10063  alephprc  10090  unialeph  10092  kmlem16  10156  cfsuc  10248  nd1  10578  nd2  10579  canthp1lem2  10644  0nnq  10915  1ne0sr  11087  pnfnre  11251  mnfnre  11253  ine0  11645  recgt0ii  12116  inelr  12198  0nnn  12244  nnunb  12464  nn0nepnf  12548  indstr  12896  1nuz2  12904  0nrp  13005  lsw0  14511  egt2lt3  16145  ruc  16182  odd2np1  16280  divalglem5  16336  bitsf1  16383  0nprm  16611  structcnvcnv  17082  fvsetsid  17097  fnpr2ob  17500  oduclatb  18456  0g0  18579  psgnunilem3  19357  zringndrg  21022  00ply1bas  21744  0ntop  22389  topnex  22481  bwth  22896  ustn0  23707  vitalilem5  25111  deg1nn0clb  25590  aaliou3lem9  25845  sinhalfpilem  25955  logdmn0  26130  dvlog  26141  ppiltx  26661  dchrisum0fno1  26994  nosgnn0i  27142  sltsolem1  27158  nolt02o  27178  nogt01o  27179  noprc  27261  oldirr  27364  leftirr  27365  rightirr  27366  axlowdim1  28197  topnfbey  29702  0ngrp  29742  dmadjrnb  31137  neldifpr1  31748  neldifpr2  31749  1nei  31939  nn0xmulclb  31962  ballotlem2  33425  bnj1304  33768  bnj110  33807  bnj98  33816  bnj1523  34020  subfacp1lem5  34113  msrrcl  34472  linedegen  35053  rankeq1o  35081  neufal  35229  neutru  35230  unqsym1  35248  onpsstopbas  35253  ordcmp  35270  onint1  35272  bj-ru0  35761  bj-ru  35763  bj-1nel0  35773  bj-0nelsngl  35790  bj-0nmoore  35931  bj-ccinftydisj  36032  relowlpssretop  36183  poimirlem16  36442  poimirlem17  36443  poimirlem18  36444  poimirlem19  36445  poimirlem20  36446  poimirlem22  36448  poimirlem30  36456  zrdivrng  36759  prtlem400  37678  equidqe  37730  sn-inelr  41282  eldioph4b  41482  jm2.23  41668  ttac  41708  sucomisnotcard  42228  clsk1indlem1  42729  rusbcALT  43131  nimnbi  43791  nimnbi2  43792  fouriersw  44882  aibnbna  45551  dtrucor3  47386