MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtand Structured version   Visualization version   GIF version

Theorem mtand 816
Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
Hypotheses
Ref Expression
mtand.1 (𝜑 → ¬ 𝜒)
mtand.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mtand (𝜑 → ¬ 𝜓)

Proof of Theorem mtand
StepHypRef Expression
1 mtand.1 . 2 (𝜑 → ¬ 𝜒)
2 mtand.2 . . 3 ((𝜑𝜓) → 𝜒)
32ex 397 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 189 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 383
This theorem is referenced by:  peano5  7236  wfrlem16  7583  sdomnsym  8241  unxpdomlem2  8321  cnfcom2lem  8762  cflim2  9287  fin23lem39  9374  isf32lem2  9378  konigthlem  9592  pythagtriplem4  15731  pythagtriplem11  15737  pythagtriplem13  15739  prmreclem1  15827  psgnunilem5  18121  sylow1lem3  18222  efgredlema  18360  efgredlemc  18365  lssvancl1  19155  lspexchn1  19344  lspindp1  19347  evlslem3  19729  zringlpirlem3  20049  reconnlem2  22850  aaliou2  24315  logdmnrp  24608  dmgmaddnn0  24974  pntpbnd1  25496  ostth2lem4  25546  ncolcom  25677  ncolrot1  25678  ncolrot2  25679  ncoltgdim2  25681  hleqnid  25724  ncolne1  25741  ncolncol  25762  miriso  25786  mirbtwnhl  25796  symquadlem  25805  ragncol  25825  mideulem2  25847  opphllem2  25861  opphllem4  25863  opphl  25867  hpgerlem  25878  lmieu  25897  2sqcoprm  29987  lmdvg  30339  ballotlemfcc  30895  ballotlemi1  30904  ballotlemii  30905  tgoldbachgtda  31079  nosepssdm  32173  nolt02olem  32181  nolt02o  32182  nosupbnd1lem3  32193  nosupbnd1lem4  32194  nosupbnd1lem5  32195  nosupbnd1lem6  32196  nocvxminlem  32230  lindsenlbs  33737  mblfinlem1  33779  lcvnbtwn  34834  ncvr1  35081  lnnat  35235  lplncvrlvol  35424  dalem39  35519  lhpocnle  35824  cdleme17b  36096  cdlemg31c  36508  lclkrlem2o  37331  lcfrlem19  37371  baerlem5amN  37526  baerlem5bmN  37527  baerlem5abmN  37528  mapdh8ab  37587  mapdh8ad  37589  mapdh8c  37591  fphpd  37906  fiphp3d  37909  pellexlem6  37924  elpell1qr2  37962  pellqrex  37969  pellfund14gap  37977  unxpwdom3  38191  dvgrat  39037  nelpr2  39782  nelpr1  39783  limcperiod  40378  sumnnodd  40380  stirlinglem5  40812  dirkercncflem2  40838  fourierdlem25  40866  fourierdlem63  40903  elaa2  40968  etransclem9  40977  etransclem41  41009  etransclem44  41012
  Copyright terms: Public domain W3C validator