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 mood that by denying affirms" - 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  845  intnan  900  intnanr  901  nexr  1811  equidqe  2229  ru  3182  neldifsn  3999  axnulALT  4416  nvel  4428  nfnid  4518  nlim0  4773  snsn0non  4833  nprrel  4877  0xp  4913  son2lpi  5223  son2lpiOLD  5228  nfunv  5446  dffv3  5684  mpt20  6155  snnex  6381  onprc  6395  ordeleqon  6399  onuninsuci  6450  orduninsuc  6453  iprc  6512  tfrlem13  6845  tfrlem14  6846  tfrlem16  6848  tfr2b  6851  tz7.44lem1  6857  sdomn2lp  7446  canth2  7460  map2xp  7477  fi0  7666  sucprcreg  7810  cantnfOLD  7919  rankxplim3  8084  alephnbtwn2  8238  alephprc  8265  unialeph  8267  kmlem16  8330  cfsuc  8422  nd1  8747  nd2  8748  canthp1lem2  8816  0nnq  9089  1ne0sr  9259  pnfnre  9421  mnfnre  9422  ine0  9776  recgt0ii  10234  inelr  10308  nnunb  10571  indstr  10919  1nuz2  10926  0nrp  11017  egt2lt3  13484  ruc  13521  n2dvds1  13578  odd2np1  13588  divalglem5  13597  bitsf1  13638  structcnvcnv  14181  fvsetsid  14195  strlemor1  14261  meet0  15303  join0  15304  oduclatb  15310  0g0  15430  psgnunilem3  15995  00ply1bas  17649  0ntop  18418  bwth  18913  ustn0  19695  vitalilem5  20992  deg1nn0clb  21504  aaliou3lem9  21759  sinhalfpilem  21868  logdmn0  22028  dvlog  22039  ppiltx  22458  dchrisum0fno1  22703  axlowdim1  23124  wlkntrllem3  23379  spthispth  23391  0ngrp  23617  zrdivrng  23838  vcoprne  23876  dmadjrnb  25229  rnlogblem  26378  ballotlem2  26785  subfacp1lem5  26986  nosgnn0i  27713  sltsolem1  27722  noprc  27735  linedegen  28087  rankeq1o  28122  unnf  28167  unnt  28168  unqsym1  28185  amosym1  28186  onpsstopbas  28190  ordcmp  28207  onint1  28209  prtlem400  28924  eldioph4b  29059  jm2.23  29254  ttac  29294  rusbcALT  29602  aibnbna  29829  bnj521  31545  bnj1304  31630  bnj110  31668  bnj98  31677  bnj1523  31879  bj-babygodel  31900  bj-1nel0  32143  bj-0nelsngl  32162  bj-ccinftydisj  32231
  Copyright terms: Public domain W3C validator