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 15 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt2i  112  nsyl3  113  tz7.44-3  6625  sdomdomtr  7199  domsdomtr  7201  infdif  8045  ackbij1b  8075  isf32lem5  8193  alephreg  8413  cfpwsdom  8415  inar1  8606  tskcard  8612  npomex  8829  recnz  10301  rpnnen1lem5  10560  fznuz  11084  uznfz  11085  seqcoll2  11668  ramub1lem1  13349  pgpfac1lem1  15587  lsppratlem6  16179  nconsubb  17439  iunconlem  17443  clscon  17446  xkohaus  17638  reconnlem1  18810  ivthlem2  19302  perfectlem1  20966  lgseisenlem1  21086  erdszelem9  24838  heiborlem8  26417  lcvntr  29509  ncvr1  29755  llnneat  29996  2atnelpln  30026  lplnneat  30027  lplnnelln  30028  3atnelvolN  30068  lvolneatN  30070  lvolnelln  30071  lvolnelpln  30072  lplncvrlvol  30098  4atexlemntlpq  30550  cdleme0nex  30772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator