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

Theorem mt2d 117
Description: Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
Hypotheses
Ref Expression
mt2d.1  |-  ( ph  ->  ch )
mt2d.2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
Assertion
Ref Expression
mt2d  |-  ( ph  ->  -.  ps )

Proof of Theorem mt2d
StepHypRef Expression
1 mt2d.1 . 2  |-  ( ph  ->  ch )
2 mt2d.2 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
32con2d 115 . 2  |-  ( ph  ->  ( ch  ->  -.  ps ) )
41, 3mpd 15 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt2i  118  nsyl3  119  tz7.44-3  6885  sdomdomtr  7465  domsdomtr  7467  infdif  8399  ackbij1b  8429  isf32lem5  8547  alephreg  8767  cfpwsdom  8769  inar1  8963  tskcard  8969  npomex  9186  recnz  10738  rpnnen1lem5  11004  fznuz  11563  uznfz  11564  seqcoll2  12238  ramub1lem1  14108  pgpfac1lem1  16597  lsppratlem6  17255  nconsubb  19049  iunconlem  19053  clscon  19056  xkohaus  19248  reconnlem1  20425  ivthlem2  20958  perfectlem1  22590  lgseisenlem1  22710  ex-natded5.8-2  23643  oddpwdc  26759  erdszelem9  27109  heiborlem8  28743  lcvntr  32767  ncvr1  33013  llnneat  33254  2atnelpln  33284  lplnneat  33285  lplnnelln  33286  3atnelvolN  33326  lvolneatN  33328  lvolnelln  33329  lvolnelpln  33330  lplncvrlvol  33356  4atexlemntlpq  33808  cdleme0nex  34030
  Copyright terms: Public domain W3C validator