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. (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  298  pm3.2ni  850  intnan  905  intnanr  906  nexr  1810  equidqe  2231  ru  3287  neldifsn  4105  axnulALT  4522  nvel  4534  nfnid  4624  nlim0  4880  snsn0non  4940  nprrel  4984  0xp  5020  son2lpi  5329  son2lpiOLD  5334  nfunv  5552  dffv3  5790  mpt20  6260  snnex  6487  onprc  6501  ordeleqon  6505  onuninsuci  6556  orduninsuc  6559  iprc  6618  tfrlem13  6954  tfrlem14  6955  tfrlem16  6957  tfr2b  6960  tz7.44lem1  6966  sdomn2lp  7555  canth2  7569  map2xp  7586  fi0  7776  sucprcreg  7920  cantnfOLD  8029  rankxplim3  8194  alephnbtwn2  8348  alephprc  8375  unialeph  8377  kmlem16  8440  cfsuc  8532  nd1  8857  nd2  8858  canthp1lem2  8926  0nnq  9199  1ne0sr  9369  pnfnre  9531  mnfnre  9532  ine0  9886  recgt0ii  10344  inelr  10418  nnunb  10681  indstr  11029  1nuz2  11036  0nrp  11127  egt2lt3  13601  ruc  13638  n2dvds1  13695  odd2np1  13705  divalglem5  13714  bitsf1  13755  structcnvcnv  14298  fvsetsid  14312  strlemor1  14379  meet0  15421  join0  15422  oduclatb  15428  0g0  15548  psgnunilem3  16116  00ply1bas  17813  0ntop  18645  bwth  19140  ustn0  19922  vitalilem5  21220  deg1nn0clb  21689  aaliou3lem9  21944  sinhalfpilem  22053  logdmn0  22213  dvlog  22224  ppiltx  22643  dchrisum0fno1  22888  axlowdim1  23352  wlkntrllem3  23607  spthispth  23619  0ngrp  23845  zrdivrng  24066  vcoprne  24104  dmadjrnb  25457  rnlogblem  26598  ballotlem2  27010  subfacp1lem5  27211  nosgnn0i  27939  sltsolem1  27948  noprc  27961  linedegen  28313  rankeq1o  28348  unnf  28392  unnt  28393  unqsym1  28410  amosym1  28411  onpsstopbas  28415  ordcmp  28432  onint1  28434  prtlem400  29158  eldioph4b  29293  jm2.23  29488  ttac  29528  rusbcALT  29836  aibnbna  30063  bnj521  32041  bnj1304  32126  bnj110  32164  bnj98  32173  bnj1523  32375  bj-babygodel  32436  bj-ru0  32748  bj-ru  32750  bj-1nel0  32758  bj-0nelsngl  32777  bj-ccinftydisj  32855
  Copyright terms: Public domain W3C validator