Theorem mto 188

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 151. (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 185	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  192  mtbi  313  intnan  476  intnanr  477  pm3.2ni  896  nexr  2228  nonconne  2997  ru  3639  neldifsn  4520  axnulALT  4988  nvel  5000  nfnid  5052  nprrel  5368  0xp  5408  son2lpi  5742  nlim0  6002  snsn0non  6062  nfunv  6137  dffv3  6407  mpt20  6958  snnexOLD  7200  onprc  7217  ordeleqon  7221  onuninsuci  7273  orduninsuc  7276  iprc  7334  tfrlem13  7725  tfrlem14  7726  tfrlem16  7728  tfr2b  7731  tz7.44lem1  7740  sdomn2lp  8341  canth2  8355  map2xp  8372  fi0  8568  sucprcreg  8748  rankxplim3  8994  alephnbtwn2  9181  alephprc  9208  unialeph  9210  kmlem16  9275  cfsuc  9367  nd1  9697  nd2  9698  canthp1lem2  9763  0nnq  10034  1ne0sr  10205  pnfnre  10369  mnfnre  10370  ine0  10753  recgt0ii  11217  inelr  11298  nnunb  11558  nn0nepnf  11640  indstr  11978  1nuz2  11986  0nrp  12082  lsw0  13567  egt2lt3  15157  ruc  15195  odd2np1  15288  n2dvds1  15327  divalglem5  15343  bitsf1  15390  structcnvcnv  16085  fvsetsid  16104  strlemor1OLD  16183  meet0  17345  join0  17346  oduclatb  17352  0g0  17471  psgnunilem3  18120  00ply1bas  19821  zringndrg  20049  0ntop  20927  topnex  21018  bwth  21431  ustn0  22241  vitalilem5  23599  deg1nn0clb  24070  aaliou3lem9  24325  sinhalfpilem  24436  logdmn0  24606  dvlog  24617  ppiltx  25123  dchrisum0fno1  25420  axlowdim1  26059  topnfbey  27662  0ngrp  27700  dmadjrnb  29099  ballotlem2  30881  bnj521  31134  bnj1304  31218  bnj110  31256  bnj98  31265  bnj1523  31467  subfacp1lem5  31494  msrrcl  31768  nosgnn0i  32138  sltsolem1  32152  nolt02o  32171  noprc  32221  linedegen  32576  rankeq1o  32604  unnf  32728  unnt  32729  unqsym1  32746  amosym1  32747  onpsstopbas  32751  ordcmp  32768  onint1  32770  bj-babygodel  32908  bj-ru0  33245  bj-ru  33247  bj-1nel0  33253  bj-0nelsngl  33271  bj-0nmoore  33380  bj-ccinftydisj  33419  relowlpssretop  33530  poimirlem16  33740  poimirlem17  33741  poimirlem18  33742  poimirlem19  33743  poimirlem20  33744  poimirlem22  33746  poimirlem30  33754  zrdivrng  34065  prtlem400  34651  equidqe  34703  eldioph4b  37878  jm2.23  38065  ttac  38105  clsk1indlem1  38844  rusbcALT  39140  fouriersw  40928  aibnbna  41556