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 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  1685  nexr  1772  equidqe  2231  ru  3128  neldifsn  3897  axnulALT  4304  nvel  4310  nfnid  4361  nlim0  4607  snsn0non  4667  snnex  4680  onprc  4732  ordeleqon  4736  onuninsuci  4787  orduninsuc  4790  nprrel  4887  xp0r  4923  iprc  5101  son2lpi  5229  son2lpiOLD  5234  nfunv  5451  dffv3  5691  mpt20  6394  tfrlem13  6618  tfrlem14  6619  tfrlem16  6621  tfr2b  6624  tz7.44lem1  6630  sdomn2lp  7213  canth2  7227  map2xp  7244  fi0  7391  cantnf  7613  rankxplim3  7769  alephnbtwn2  7917  alephprc  7944  unialeph  7946  kmlem16  8009  cfsuc  8101  nd1  8426  nd2  8427  canthp1lem2  8492  0nnq  8765  1ne0sr  8935  pnfnre  9091  mnfnre  9092  ine0  9433  recgt0ii  9880  inelr  9954  nnunb  10181  indstr  10509  1nuz2  10515  0nrp  10606  egt2lt3  12768  ruc  12805  odd2np1  12871  divalglem5  12880  bitsfzolem  12909  bitsfzo  12910  bitsinv1lem  12916  bitsf1  12921  structcnvcnv  13443  strlemor1  13519  oduclatb  14534  0g0  14672  00ply1bas  16597  0ntop  16941  ustn0  18211  vitalilem5  19465  deg1nn0clb  19974  aaliou3lem9  20228  sinhalfpilem  20335  logdmn0  20492  dvlog  20503  ppiltx  20921  dchrisum0fno1  21166  wlkntrllem3  21522  spthispth  21534  0ngrp  21760  zrdivrng  21981  vcoprne  22019  dmadjrnb  23370  rnlogblem  24360  ballotlem2  24707  subfacp1lem5  24831  nosgnn0i  25535  sltsolem1  25544  noprc  25557  axlowdim1  25810  linedegen  25989  rankeq1o  26024  unnf  26069  unnt  26070  unqsym1  26087  amosym1  26088  onpsstopbas  26092  ordcmp  26109  onint1  26111  prtlem400  26617  eldioph4b  26770  jm2.23  26965  ttac  27005  psgnunilem3  27295  rusbcALT  27515  aibnbna  27749  bnj521  28822  bnj1304  28909  bnj110  28947  bnj98  28956  bnj1523  29158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator