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

Theorem mtand 663
Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
Hypotheses
Ref Expression
mtand.1  |-  ( ph  ->  -.  ch )
mtand.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mtand  |-  ( ph  ->  -.  ps )

Proof of Theorem mtand
StepHypRef Expression
1 mtand.1 . 2  |-  ( ph  ->  -.  ch )
2 mtand.2 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
32ex 435 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 180 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  peano5  6721  wfrlem16  7050  sdomnsym  7694  unxpdomlem2  7774  cnfcom2lem  8196  cflim2  8682  fin23lem39  8769  isf32lem2  8773  konigthlem  8982  pythagtriplem4  14721  pythagtriplem11  14727  pythagtriplem13  14729  prmreclem1  14812  psgnunilem5  17079  sylow1lem3  17180  efgredlema  17318  efgredlemc  17323  lssvancl1  18096  lspexchn1  18281  lspindp1  18284  evlslem3  18665  zringlpirlem3  18982  reconnlem2  21769  aaliou2  23187  logdmnrp  23477  dmgmaddnn0  23843  pntpbnd1  24313  ostth2lem4  24363  ncolcom  24492  ncolrot1  24493  ncolrot2  24494  ncoltgdim2  24496  hleqnid  24539  ncolne1  24555  ncolncol  24576  miriso  24600  mirbtwnhl  24610  symquadlem  24617  ragncol  24637  mideulem2  24659  opphllem4  24675  opphl  24679  hpgerlem  24689  lmieu  24708  2sqcoprm  28272  lmdvg  28624  ballotlemfcc  29178  ballotlemi1  29187  ballotlemii  29188  nocvxminlem  30390  mblfinlem1  31710  lcvnbtwn  32329  ncvr1  32576  lnnat  32730  lplncvrlvol  32919  dalem39  33014  lhpocnle  33319  cdleme17b  33591  cdlemg31c  34004  lclkrlem2o  34827  lcfrlem19  34867  baerlem5amN  35022  baerlem5bmN  35023  baerlem5abmN  35024  mapdh8ab  35083  mapdh8ad  35085  mapdh8c  35087  fphpd  35397  fiphp3d  35400  pellexlem6  35417  elpell1qr2  35457  pellqrex  35465  pellfund14gap  35474  unxpwdom3  35692  dvgrat  36331  limcperiod  37313  sumnnodd  37315  stirlinglem5  37542  dirkercncflem2  37568  fourierdlem25  37596  fourierdlem63  37634  etransclem9  37708  etransclem41  37740  etransclem44  37743
  Copyright terms: Public domain W3C validator