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

Theorem mt2d 111
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 109 . 2  |-  ( ph  ->  ( ch  ->  -.  ps ) )
41, 3mpd 16 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt2i  112  nsyl3  113  tz7.44-3  6416  sdomdomtr  6989  domsdomtr  6991  infdif  7830  ackbij1b  7860  isf32lem5  7978  alephreg  8199  cfpwsdom  8201  inar1  8392  tskcard  8398  npomex  8615  recnz  10082  rpnnen1lem5  10341  fznuz  10858  uznfz  10859  seqcoll2  11396  ramub1lem1  13067  pgpfac1lem1  15303  lsppratlem6  15899  nconsubb  17143  iunconlem  17147  clscon  17150  xkohaus  17341  reconnlem1  18325  ivthlem2  18806  perfectlem1  20462  lgseisenlem1  20582  ex-natded5.8-2  20821  erdszelem9  23134  heiborlem8  25941  lcvntr  28483  ncvr1  28729  llnneat  28970  2atnelpln  29000  lplnneat  29001  lplnnelln  29002  3atnelvolN  29042  lvolneatN  29044  lvolnelln  29045  lvolnelpln  29046  lplncvrlvol  29072  4atexlemntlpq  29524  cdleme0nex  29746
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator