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

Theorem mto 167
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 10 . 2  |-  ( ph  ->  -.  ps )
41, 3pm2.65i 165 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3  171  mtbi  289  pm3.2ni  827  intnan  880  intnanr  881  equid  1644  nexr  1820  equidqe  2112  ru  2990  neldifsn  3751  axnulALT  4147  nvel  4153  nfnid  4204  nlim0  4450  snsn0non  4511  snnex  4524  onprc  4576  ordeleqon  4580  onuninsuci  4631  orduninsuc  4634  nprrel  4731  xp0r  4768  iprc  4943  son2lpi  5071  son2lpiOLD  5076  nfunv  5285  dffv3  5521  mpt20  6199  tfrlem13  6406  tfrlem14  6407  tfrlem16  6409  tfr2b  6412  tz7.44lem1  6418  sdomn2lp  7000  canth2  7014  map2xp  7031  fi0  7173  cantnf  7395  rankxplim3  7551  alephnbtwn2  7699  alephprc  7726  unialeph  7728  kmlem16  7791  cfsuc  7883  nd1  8209  nd2  8210  canthp1lem2  8275  0nnq  8548  1ne0sr  8718  pnfnre  8874  mnfnre  8875  ine0  9215  recgt0ii  9662  inelr  9736  nnunb  9961  indstr  10287  1nuz2  10293  0nrp  10384  egt2lt3  12484  ruc  12521  odd2np1  12587  divalglem5  12596  bitsfzolem  12625  bitsfzo  12626  bitsinv1lem  12632  bitsf1  12637  smu02  12678  structcnvcnv  13159  strlemor1  13235  oduclatb  14248  0g0  14386  00ply1bas  16318  0ntop  16651  vitalilem5  18967  deg1nn0clb  19476  aaliou3lem9  19730  sinhalfpilem  19834  logdmn0  19987  dvlog  19998  ppiltx  20415  dchrisum0fno1  20660  0ngrp  20878  zrdivrng  21099  vcoprne  21135  dmadjrnb  22486  rnlogblem  23401  subfacp1lem5  23715  nosgnn0i  24313  sltsolem1  24322  noprc  24335  funpartfv  24483  axlowdim1  24587  linedegen  24766  rankeq1o  24801  unnf  24846  unnt  24847  unqsym1  24864  amosym1  24865  onpsstopbas  24869  ordcmp  24886  onint1  24888  inpc  25277  zrfld  25435  prtlem400  26738  eldioph4b  26894  jm2.23  27089  ttac  27129  psgnunilem3  27419  rusbcALT  27639  compneOLD  27643  bnj521  28765  bnj1304  28852  bnj110  28890  bnj98  28899  bnj1523  29101  ax9lem1  29140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator