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

Theorem mtand 692
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 449 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 189 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383
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 385
This theorem is referenced by:  peano5  7131  wfrlem16  7475  sdomnsym  8126  unxpdomlem2  8206  cnfcom2lem  8636  cflim2  9123  fin23lem39  9210  isf32lem2  9214  konigthlem  9428  pythagtriplem4  15571  pythagtriplem11  15577  pythagtriplem13  15579  prmreclem1  15667  psgnunilem5  17960  sylow1lem3  18061  efgredlema  18199  efgredlemc  18204  lssvancl1  18993  lspexchn1  19178  lspindp1  19181  evlslem3  19562  zringlpirlem3  19882  reconnlem2  22677  aaliou2  24140  logdmnrp  24432  dmgmaddnn0  24798  pntpbnd1  25320  ostth2lem4  25370  ncolcom  25501  ncolrot1  25502  ncolrot2  25503  ncoltgdim2  25505  hleqnid  25548  ncolne1  25565  ncolncol  25586  miriso  25610  mirbtwnhl  25620  symquadlem  25629  ragncol  25649  mideulem2  25671  opphllem2  25685  opphllem4  25687  opphl  25691  hpgerlem  25702  lmieu  25721  2sqcoprm  29775  lmdvg  30127  ballotlemfcc  30683  ballotlemi1  30692  ballotlemii  30693  tgoldbachgtda  30867  nosepssdm  31961  nolt02olem  31969  nolt02o  31970  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd1lem6  31984  nocvxminlem  32018  lindsenlbs  33534  mblfinlem1  33576  lcvnbtwn  34630  ncvr1  34877  lnnat  35031  lplncvrlvol  35220  dalem39  35315  lhpocnle  35620  cdleme17b  35892  cdlemg31c  36304  lclkrlem2o  37127  lcfrlem19  37167  baerlem5amN  37322  baerlem5bmN  37323  baerlem5abmN  37324  mapdh8ab  37383  mapdh8ad  37385  mapdh8c  37387  fphpd  37697  fiphp3d  37700  pellexlem6  37715  elpell1qr2  37753  pellqrex  37760  pellfund14gap  37768  unxpwdom3  37982  dvgrat  38828  nelpr2  39575  nelpr1  39576  limcperiod  40178  sumnnodd  40180  stirlinglem5  40613  dirkercncflem2  40639  fourierdlem25  40667  fourierdlem63  40704  elaa2  40769  etransclem9  40778  etransclem41  40810  etransclem44  40813
  Copyright terms: Public domain W3C validator