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  485  intnanr  486  pm3.2ni  878  nexr  2180  nonconne  2941  ru  3772  noelOLD  4331  reu0  4358  neldifsn  4797  axnulALT  5305  nvel  5317  nfnid  5375  nprrel  5737  0xp  5776  son2lpi  6135  nlim0  6430  snsn0non  6496  onnev  6498  nfunv  6587  dffv3  6892  mpo0  7505  onprc  7781  ordeleqon  7785  onuninsuci  7845  orduninsuc  7848  iprc  7919  poxp2  8148  poxp3  8155  tfrlem13  8411  tfrlem14  8412  tfrlem16  8414  tfr2b  8417  tz7.44lem1  8426  nlim1  8510  nlim2  8511  sdomn2lp  9141  canth2  9155  map2xp  9172  snnen2o  9262  1sdom2dom  9272  fi0  9445  sucprcreg  9626  rankxplim3  9906  alephnbtwn2  10097  alephprc  10124  unialeph  10126  kmlem16  10190  cfsuc  10282  nd1  10612  nd2  10613  canthp1lem2  10678  0nnq  10949  1ne0sr  11121  pnfnre  11287  mnfnre  11289  ine0  11681  recgt0ii  12153  inelr  12235  0nnn  12281  nnunb  12501  nn0nepnf  12585  indstr  12933  1nuz2  12941  0nrp  13044  lsw0  14551  egt2lt3  16186  ruc  16223  odd2np1  16321  divalglem5  16377  bitsf1  16424  0nprm  16652  structcnvcnv  17125  fvsetsid  17140  fnpr2ob  17543  oduclatb  18502  0g0  18627  psgnunilem3  19463  zringndrg  21411  00ply1bas  22182  0ntop  22851  topnex  22943  bwth  23358  ustn0  24169  vitalilem5  25585  deg1nn0clb  26070  aaliou3lem9  26330  sinhalfpilem  26443  logdmn0  26619  dvlog  26630  ppiltx  27154  dchrisum0fno1  27489  nosgnn0i  27638  sltsolem1  27654  nolt02o  27674  nogt01o  27675  noprc  27758  oldirr  27862  leftirr  27863  rightirr  27864  axlowdim1  28842  topnfbey  30351  0ngrp  30393  dmadjrnb  31788  neldifpr1  32408  neldifpr2  32409  1nei  32600  nn0xmulclb  32623  ballotlem2  34239  bnj1304  34581  bnj110  34620  bnj98  34629  bnj1523  34833  subfacp1lem5  34925  msrrcl  35284  linedegen  35870  rankeq1o  35898  neufal  36021  neutru  36022  unqsym1  36040  onpsstopbas  36045  ordcmp  36062  onint1  36064  bj-ru0  36552  bj-ru  36554  bj-1nel0  36564  bj-0nelsngl  36581  bj-0nmoore  36722  bj-ccinftydisj  36823  relowlpssretop  36974  poimirlem16  37240  poimirlem17  37241  poimirlem18  37242  poimirlem19  37243  poimirlem20  37244  poimirlem22  37246  poimirlem30  37254  zrdivrng  37557  prtlem400  38472  equidqe  38524  sn-inelr  42155  eldioph4b  42373  jm2.23  42559  ttac  42599  sucomisnotcard  43116  clsk1indlem1  43617  rusbcALT  44018  nimnbi  44674  nimnbi2  44675  fouriersw  45757  aibnbna  46426  dtrucor3  48057