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  1684  nexr  1768  equidqe  2200  ru  3096  neldifsn  3865  axnulALT  4270  nvel  4276  nfnid  4327  nlim0  4573  snsn0non  4633  snnex  4646  onprc  4698  ordeleqon  4702  onuninsuci  4753  orduninsuc  4756  nprrel  4853  xp0r  4889  iprc  5067  son2lpi  5195  son2lpiOLD  5200  nfunv  5417  dffv3  5657  mpt20  6359  tfrlem13  6580  tfrlem14  6581  tfrlem16  6583  tfr2b  6586  tz7.44lem1  6592  sdomn2lp  7175  canth2  7189  map2xp  7206  fi0  7353  cantnf  7575  rankxplim3  7731  alephnbtwn2  7879  alephprc  7906  unialeph  7908  kmlem16  7971  cfsuc  8063  nd1  8388  nd2  8389  canthp1lem2  8454  0nnq  8727  1ne0sr  8897  pnfnre  9053  mnfnre  9054  ine0  9394  recgt0ii  9841  inelr  9915  nnunb  10142  indstr  10470  1nuz2  10476  0nrp  10567  egt2lt3  12725  ruc  12762  odd2np1  12828  divalglem5  12837  bitsfzolem  12866  bitsfzo  12867  bitsinv1lem  12873  bitsf1  12878  structcnvcnv  13400  strlemor1  13476  oduclatb  14491  0g0  14629  00ply1bas  16554  0ntop  16894  ustn0  18164  vitalilem5  19364  deg1nn0clb  19873  aaliou3lem9  20127  sinhalfpilem  20234  logdmn0  20391  dvlog  20402  ppiltx  20820  dchrisum0fno1  21065  wlkntrllem5  21410  spthispth  21420  0ngrp  21640  zrdivrng  21861  vcoprne  21899  dmadjrnb  23250  rnlogblem  24188  ballotlem2  24518  subfacp1lem5  24642  nosgnn0i  25330  sltsolem1  25339  noprc  25352  axlowdim1  25605  linedegen  25784  rankeq1o  25819  unnf  25864  unnt  25865  unqsym1  25882  amosym1  25883  onpsstopbas  25887  ordcmp  25904  onint1  25906  prtlem400  26403  eldioph4b  26556  jm2.23  26751  ttac  26791  psgnunilem3  27081  rusbcALT  27301  aibnbna  27535  bnj521  28435  bnj1304  28522  bnj110  28560  bnj98  28569  bnj1523  28771  ax9lem1  29116
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator