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  6307  sdomdomtr  6879  domsdomtr  6881  infdif  7719  ackbij1b  7749  isf32lem5  7867  alephreg  8084  cfpwsdom  8086  inar1  8277  tskcard  8283  npomex  8500  recnz  9966  rpnnen1lem5  10225  fznuz  10742  uznfz  10743  seqcoll2  11279  ramub1lem1  12947  pgpfac1lem1  15144  lsppratlem6  15739  nconsubb  16981  iunconlem  16985  clscon  16988  xkohaus  17179  reconnlem1  18163  ivthlem2  18644  perfectlem1  20300  lgseisenlem1  20420  ex-natded5.8-2  20659  erdszelem9  22901  heiborlem8  25708  lcvntr  27905  ncvr1  28151  llnneat  28392  2atnelpln  28422  lplnneat  28423  lplnnelln  28424  3atnelvolN  28464  lvolneatN  28466  lvolnelln  28467  lvolnelpln  28468  lplncvrlvol  28494  4atexlemntlpq  28946  cdleme0nex  29168
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator