MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mto Unicode version

Theorem mto 176
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 135. (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
StepHypRef Expression
1 mto.2 . 2
2 mto.1 . . 3
32a1i 11 . 2
41, 3pm2.65i 173 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  mt3  180  mtbi  298  pm3.2ni  854  intnan  914  intnanr  915  nexr  1872  equidqe  2252  nonconne  2665  ru  3326  neldifsn  4157  axnulALT  4579  nvel  4591  nfnid  4681  nlim0  4941  snsn0non  5001  nprrel  5047  0xp  5085  son2lpi  5400  son2lpiOLD  5405  nfunv  5624  dffv3  5867  mpt20  6367  snnex  6606  onprc  6620  ordeleqon  6624  onuninsuci  6675  orduninsuc  6678  iprc  6735  tfrlem13  7078  tfrlem14  7079  tfrlem16  7081  tfr2b  7084  tz7.44lem1  7090  sdomn2lp  7676  canth2  7690  map2xp  7707  fi0  7900  sucprcreg  8046  cantnfOLD  8155  rankxplim3  8320  alephnbtwn2  8474  alephprc  8501  unialeph  8503  kmlem16  8566  cfsuc  8658  nd1  8983  nd2  8984  canthp1lem2  9052  0nnq  9323  1ne0sr  9494  pnfnre  9656  mnfnre  9657  ine0  10017  recgt0ii  10476  inelr  10551  nnunb  10816  indstr  11179  1nuz2  11186  0nrp  11279  egt2lt3  13939  ruc  13976  n2dvds1  14035  odd2np1  14046  divalglem5  14055  bitsf1  14096  structcnvcnv  14643  fvsetsid  14657  strlemor1  14724  meet0  15767  join0  15768  oduclatb  15774  0g0  15890  psgnunilem3  16521  00ply1bas  18281  0ntop  19414  bwth  19910  ustn0  20723  vitalilem5  22021  deg1nn0clb  22490  aaliou3lem9  22746  sinhalfpilem  22856  logdmn0  23021  dvlog  23032  ppiltx  23451  dchrisum0fno1  23696  axlowdim1  24262  wlkntrllem3  24563  spthispth  24575  0ngrp  25213  zrdivrng  25434  vcoprne  25472  dmadjrnb  26825  rnlogblem  28015  ballotlem2  28427  subfacp1lem5  28628  msrrcl  28903  nosgnn0i  29419  sltsolem1  29428  noprc  29441  linedegen  29793  rankeq1o  29828  unnf  29872  unnt  29873  unqsym1  29890  amosym1  29891  onpsstopbas  29895  ordcmp  29912  onint1  29914  prtlem400  30611  eldioph4b  30745  jm2.23  30938  ttac  30978  rusbcALT  31346  fouriersw  32014  aibnbna  32101  bnj521  33792  bnj1304  33878  bnj110  33916  bnj98  33925  bnj1523  34127  bj-babygodel  34191  bj-ru0  34500  bj-ru  34502  bj-1nel0  34510  bj-0nelsngl  34529  bj-ccinftydisj  34616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator