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

Theorem mtand 659
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 434 . 2
41, 3mtod 177 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369
This theorem is referenced by:  peano5  6723  sdomnsym  7662  unxpdomlem2  7745  cnfcom2lem  8166  cnfcom2lemOLD  8174  cflim2  8664  fin23lem39  8751  isf32lem2  8755  konigthlem  8964  pythagtriplem4  14343  pythagtriplem11  14349  pythagtriplem13  14351  prmreclem1  14434  psgnunilem5  16519  sylow1lem3  16620  efgredlema  16758  efgredlemc  16763  lssvancl1  17591  lspexchn1  17776  lspindp1  17779  evlslem3  18183  zringlpirlem3  18511  zlpirlem3  18516  reconnlem2  21332  aaliou2  22736  logdmnrp  23022  pntpbnd1  23771  ostth2lem4  23821  ncolcom  23948  ncolrot1  23949  ncolrot2  23950  ncoltgdim2  23952  hleqnid  23992  ncolne1  24005  ncolncol  24026  miriso  24050  mirbtwnhl  24060  symquadlem  24066  ragncol  24086  mideulem2  24108  opphllem4  24122  opphl  24125  hpgerlem  24134  lmieu  24150  2sqcoprm  27635  lmdvg  27935  ballotlemfcc  28432  ballotlemi1  28441  ballotlemii  28442  dmgmaddnn0  28569  wfrlem16  29358  nocvxminlem  29450  mblfinlem1  30051  fphpd  30750  fiphp3d  30753  pellexlem6  30770  elpell1qr2  30808  pellqrex  30815  pellfund14gap  30823  unxpwdom3  31041  dvgrat  31193  limcperiod  31634  sumnnodd  31636  stirlinglem5  31860  dirkercncflem2  31886  fourierdlem25  31914  fourierdlem63  31952  etransclem9  32026  etransclem41  32058  etransclem44  32061  lcvnbtwn  34750  ncvr1  34997  lnnat  35151  lplncvrlvol  35340  dalem39  35435  lhpocnle  35740  cdleme17b  36012  cdlemg31c  36425  lclkrlem2o  37248  lcfrlem19  37288  baerlem5amN  37443  baerlem5bmN  37444  baerlem5abmN  37445  mapdh8ab  37504  mapdh8ad  37506  mapdh8c  37508
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 185  df-an 371
  Copyright terms: Public domain W3C validator