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  6504  sdomnsym  7441  unxpdomlem2  7523  cnfcom2lem  7939  cnfcom2lemOLD  7947  cflim2  8437  fin23lem39  8524  isf32lem2  8528  konigthlem  8737  pythagtriplem4  13891  pythagtriplem11  13897  pythagtriplem13  13899  prmreclem1  13982  psgnunilem5  16005  sylow1lem3  16104  efgredlema  16242  efgredlemc  16247  lssvancl1  17031  lspexchn1  17216  lspindp1  17219  evlslem3  17605  zringlpirlem3  17910  zlpirlem3  17915  reconnlem2  20409  aaliou2  21811  logdmnrp  22091  pntpbnd1  22840  ostth2lem4  22890  ncolcom  23000  ncolrot1  23001  ncolrot2  23002  ncolne1  23037  miriso  23078  symquadlem  23088  lmdvg  26388  ballotlemfcc  26881  ballotlemi1  26890  ballotlemii  26891  dmgmaddnn0  27018  wfrlem16  27744  nocvxminlem  27836  mblfinlem1  28433  fphpd  29160  fiphp3d  29163  pellexlem6  29180  elpell1qr2  29218  pellqrex  29225  pellfund14gap  29233  unxpwdom3  29453  stirlinglem5  29878  lcvnbtwn  32675  ncvr1  32922  lnnat  33076  lplncvrlvol  33265  dalem39  33360  lhpocnle  33665  cdleme17b  33936  cdlemg31c  34348  lclkrlem2o  35171  lcfrlem19  35211  baerlem5amN  35366  baerlem5bmN  35367  baerlem5abmN  35368  mapdh8ab  35427  mapdh8ad  35429  mapdh8c  35431
  Copyright terms: Public domain W3C validator