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  852  intnan  912  intnanr  913  nexr  1856  equidqe  2236  nonconne  2649  ru  3310  neldifsn  4138  axnulALT  4560  nvel  4572  nfnid  4662  nlim0  4922  snsn0non  4982  nprrel  5028  0xp  5066  son2lpi  5381  son2lpiOLD  5386  nfunv  5605  dffv3  5848  mpt20  6348  snnex  6587  onprc  6601  ordeleqon  6605  onuninsuci  6656  orduninsuc  6659  iprc  6716  tfrlem13  7057  tfrlem14  7058  tfrlem16  7060  tfr2b  7063  tz7.44lem1  7069  sdomn2lp  7654  canth2  7668  map2xp  7685  fi0  7878  sucprcreg  8023  cantnfOLD  8132  rankxplim3  8297  alephnbtwn2  8451  alephprc  8478  unialeph  8480  kmlem16  8543  cfsuc  8635  nd1  8960  nd2  8961  canthp1lem2  9029  0nnq  9300  1ne0sr  9471  pnfnre  9633  mnfnre  9634  ine0  9993  recgt0ii  10452  inelr  10527  nnunb  10792  indstr  11154  1nuz2  11161  0nrp  11254  egt2lt3  13811  ruc  13848  n2dvds1  13907  odd2np1  13918  divalglem5  13927  bitsf1  13968  structcnvcnv  14515  fvsetsid  14529  strlemor1  14596  meet0  15636  join0  15637  oduclatb  15643  0g0  15759  psgnunilem3  16390  00ply1bas  18149  0ntop  19281  bwth  19776  ustn0  20589  vitalilem5  21887  deg1nn0clb  22356  aaliou3lem9  22611  sinhalfpilem  22721  logdmn0  22886  dvlog  22897  ppiltx  23316  dchrisum0fno1  23561  axlowdim1  24127  wlkntrllem3  24428  spthispth  24440  0ngrp  25078  zrdivrng  25299  vcoprne  25337  dmadjrnb  26690  rnlogblem  27881  ballotlem2  28293  subfacp1lem5  28494  msrrcl  28769  nosgnn0i  29387  sltsolem1  29396  noprc  29409  linedegen  29761  rankeq1o  29796  unnf  29840  unnt  29841  unqsym1  29858  amosym1  29859  onpsstopbas  29863  ordcmp  29880  onint1  29882  prtlem400  30579  eldioph4b  30713  jm2.23  30906  ttac  30946  rusbcALT  31293  fouriersw  31899  aibnbna  31935  bnj521  33500  bnj1304  33585  bnj110  33623  bnj98  33632  bnj1523  33834  bj-babygodel  33905  bj-ru0  34212  bj-ru  34214  bj-1nel0  34222  bj-0nelsngl  34241  bj-ccinftydisj  34318
  Copyright terms: Public domain W3C validator