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

Theorem mtand 659
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 434 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 177 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
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
This theorem is referenced by:  peano5  6707  sdomnsym  7642  unxpdomlem2  7725  cnfcom2lem  8145  cnfcom2lemOLD  8153  cflim2  8643  fin23lem39  8730  isf32lem2  8734  konigthlem  8943  pythagtriplem4  14202  pythagtriplem11  14208  pythagtriplem13  14210  prmreclem1  14293  psgnunilem5  16325  sylow1lem3  16426  efgredlema  16564  efgredlemc  16569  lssvancl1  17391  lspexchn1  17576  lspindp1  17579  evlslem3  17982  zringlpirlem3  18306  zlpirlem3  18311  reconnlem2  21095  aaliou2  22498  logdmnrp  22778  pntpbnd1  23527  ostth2lem4  23577  ncolcom  23704  ncolrot1  23705  ncolrot2  23706  ncolne1  23747  miriso  23791  symquadlem  23802  lmdvg  27599  ballotlemfcc  28100  ballotlemi1  28109  ballotlemii  28110  dmgmaddnn0  28237  wfrlem16  28963  nocvxminlem  29055  mblfinlem1  29656  fphpd  30382  fiphp3d  30385  pellexlem6  30402  elpell1qr2  30440  pellqrex  30447  pellfund14gap  30455  unxpwdom3  30673  stirlinglem5  31406  lcvnbtwn  33840  ncvr1  34087  lnnat  34241  lplncvrlvol  34430  dalem39  34525  lhpocnle  34830  cdleme17b  35101  cdlemg31c  35513  lclkrlem2o  36336  lcfrlem19  36376  baerlem5amN  36531  baerlem5bmN  36532  baerlem5abmN  36533  mapdh8ab  36592  mapdh8ad  36594  mapdh8c  36596
  Copyright terms: Public domain W3C validator