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

Theorem mto 176
Description: The rule of modus tollens. The rule says, "if 
ps is not true, and  ph implies  ps, then  ph 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  |-  -.  ps
mto.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
mto  |-  -.  ph

Proof of Theorem mto
StepHypRef Expression
1 mto.2 . 2  |-  ( ph  ->  ps )
2 mto.1 . . 3  |-  -.  ps
32a1i 11 . 2  |-  ( ph  ->  -.  ps )
41, 3pm2.65i 173 1  |-  -.  ph
Colors of variables: wff setvar class
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  180  mtbi  296  pm3.2ni  852  intnan  912  intnanr  913  nexr  1880  nonconne  2590  ru  3251  neldifsn  4071  axnulALT  4494  nvel  4504  nfnid  4591  nlim0  4850  snsn0non  4910  nprrel  4956  0xp  4994  son2lpi  5308  nfunv  5527  dffv3  5770  mpt20  6266  snnex  6505  onprc  6519  ordeleqon  6523  onuninsuci  6574  orduninsuc  6577  iprc  6634  tfrlem13  6977  tfrlem14  6978  tfrlem16  6980  tfr2b  6983  tz7.44lem1  6989  sdomn2lp  7575  canth2  7589  map2xp  7606  fi0  7795  sucprcreg  7940  cantnfOLD  8047  rankxplim3  8212  alephnbtwn2  8366  alephprc  8393  unialeph  8395  kmlem16  8458  cfsuc  8550  nd1  8875  nd2  8876  canthp1lem2  8942  0nnq  9213  1ne0sr  9384  pnfnre  9546  mnfnre  9547  ine0  9910  recgt0ii  10367  inelr  10442  nnunb  10708  indstr  11069  1nuz2  11076  0nrp  11170  zgt1rpn0n1  11176  lsw0  12494  egt2lt3  13941  ruc  13978  n2dvds1  14037  odd2np1  14048  divalglem5  14057  bitsf1  14098  structcnvcnv  14645  fvsetsid  14661  strlemor1  14729  meet0  15884  join0  15885  oduclatb  15891  0g0  16007  psgnunilem3  16638  00ply1bas  18394  0ntop  19499  bwth  19996  ustn0  20808  vitalilem5  22106  deg1nn0clb  22575  aaliou3lem9  22831  sinhalfpilem  22941  logdmn0  23108  dvlog  23119  ppiltx  23568  dchrisum0fno1  23813  axlowdim1  24383  wlkntrllem3  24684  spthispth  24696  0ngrp  25330  zrdivrng  25551  vcoprne  25589  dmadjrnb  26941  ballotlem2  28610  subfacp1lem5  28817  msrrcl  29092  nosgnn0i  29584  sltsolem1  29593  noprc  29606  linedegen  29946  rankeq1o  29981  unnf  30025  unnt  30026  unqsym1  30043  amosym1  30044  onpsstopbas  30048  ordcmp  30065  onint1  30067  prtlem400  30777  eldioph4b  30910  jm2.23  31104  ttac  31144  rusbcALT  31514  fouriersw  32180  aibnbna  32267  bnj521  34139  bnj1304  34225  bnj110  34263  bnj98  34272  bnj1523  34474  bj-babygodel  34538  bj-ru0  34848  bj-ru  34850  bj-1nel0  34858  bj-0nelsngl  34877  bj-ccinftydisj  34963  equidqe  35065
  Copyright terms: Public domain W3C validator