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

Theorem mto 169
Description: The rule of modus tollens. The rule says, "if 
ps is not true, and  ph implies  ps, then  ps must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 10. (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 12 . 2  |-  ( ph  ->  -.  ps )
41, 3pm2.65i 167 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt3  173  mtbi  291  pm3.2ni  830  intnan  885  intnanr  886  ax12o10lem1  1635  equidqe  1686  nexr  1804  ru  2934  neldifsn  3692  axnulALT  4087  nvel  4093  nfnid  4142  nlim0  4387  snsn0non  4448  snnex  4461  onprc  4513  ordeleqon  4517  onuninsuci  4568  orduninsuc  4571  nprrel  4684  xp0r  4721  iprc  4896  son2lpi  5024  son2lpiOLD  5029  nfunv  5189  mpt20  6098  tfrlem13  6339  tfrlem14  6340  tfrlem16  6342  tfr2b  6345  tz7.44lem1  6351  sdomn2lp  6933  canth2  6947  map2xp  6964  fi0  7106  cantnf  7328  rankxplim3  7484  alephnbtwn2  7632  alephprc  7659  unialeph  7661  kmlem16  7724  cfsuc  7816  nd1  8142  nd2  8143  canthp1lem2  8208  0nnq  8481  1ne0sr  8651  pnfnre  8807  mnfnre  8808  ine0  9148  recgt0ii  9595  inelr  9669  nnunb  9893  indstr  10219  1nuz2  10225  0nrp  10316  egt2lt3  12411  ruc  12448  odd2np1  12514  divalglem5  12523  bitsfzolem  12552  bitsfzo  12553  bitsinv1lem  12559  bitsf1  12564  smu02  12605  structcnvcnv  13086  strlemor1  13162  oduclatb  14175  0g0  14313  00ply1bas  16245  0ntop  16578  vitalilem5  18894  deg1nn0clb  19403  aaliou3lem9  19657  sinhalfpilem  19761  logdmn0  19914  dvlog  19925  ppiltx  20342  dchrisum0fno1  20587  0ngrp  20803  zrdivrng  21024  vcoprne  21060  dmadjrnb  22411  subfacp1lem5  23052  nosgnn0i  23646  axsltsolem1  23655  noprc  23668  funpartfv  23823  axlowdim1  23927  linedegen  24106  rankeq1o  24141  unnf  24186  unnt  24187  unqsym1  24204  amosym1  24205  onpsstopbas  24209  ordcmp  24226  onint1  24228  inpc  24609  zrfld  24767  prtlem400  26070  eldioph4b  26226  jm2.23  26421  ttac  26461  psgnunilem3  26751  rusbcALT  26972  compneOLD  26976  bnj521  27777  bnj1304  27864  bnj110  27902  bnj98  27911  bnj1523  28113  equidK  28115  ax12o10lem1X  28162  ax9lem1  28270
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator