MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mto Structured version   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" - remark in [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 8. (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 167 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3  173  mtbi  290  pm3.2ni  828  intnan  881  intnanr  882  equidOLD  1689  nexr  1776  equidqe  2249  ru  3152  neldifsn  3921  axnulALT  4328  nvel  4334  nfnid  4385  nlim0  4631  snsn0non  4692  snnex  4705  onprc  4757  ordeleqon  4761  onuninsuci  4812  orduninsuc  4815  nprrel  4912  xp0r  4948  iprc  5126  son2lpi  5254  son2lpiOLD  5259  nfunv  5476  dffv3  5716  mpt20  6419  tfrlem13  6643  tfrlem14  6644  tfrlem16  6646  tfr2b  6649  tz7.44lem1  6655  sdomn2lp  7238  canth2  7252  map2xp  7269  fi0  7417  cantnf  7641  rankxplim3  7797  alephnbtwn2  7945  alephprc  7972  unialeph  7974  kmlem16  8037  cfsuc  8129  nd1  8454  nd2  8455  canthp1lem2  8520  0nnq  8793  1ne0sr  8963  pnfnre  9119  mnfnre  9120  ine0  9461  recgt0ii  9908  inelr  9982  nnunb  10209  indstr  10537  1nuz2  10543  0nrp  10634  egt2lt3  12797  ruc  12834  odd2np1  12900  divalglem5  12909  bitsfzolem  12938  bitsfzo  12939  bitsinv1lem  12945  bitsf1  12950  structcnvcnv  13472  strlemor1  13548  oduclatb  14563  0g0  14701  00ply1bas  16626  0ntop  16970  ustn0  18242  vitalilem5  19496  deg1nn0clb  20005  aaliou3lem9  20259  sinhalfpilem  20366  logdmn0  20523  dvlog  20534  ppiltx  20952  dchrisum0fno1  21197  wlkntrllem3  21553  spthispth  21565  0ngrp  21791  zrdivrng  22012  vcoprne  22050  dmadjrnb  23401  rnlogblem  24391  ballotlem2  24738  subfacp1lem5  24862  nosgnn0i  25606  sltsolem1  25615  noprc  25628  axlowdim1  25890  linedegen  26069  rankeq1o  26104  unnf  26149  unnt  26150  unqsym1  26167  amosym1  26168  onpsstopbas  26172  ordcmp  26189  onint1  26191  prtlem400  26710  eldioph4b  26863  jm2.23  27058  ttac  27098  psgnunilem3  27387  rusbcALT  27607  aibnbna  27841  bnj521  29041  bnj1304  29128  bnj110  29166  bnj98  29175  bnj1523  29377  ax7w11AUX7  29600
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator