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

Theorem mt2d 109
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 107 . 2  |-  ( ph  ->  ( ch  ->  -.  ps ) )
41, 3mpd 14 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt2i  110  nsyl3  111  tz7.44-3  6421  sdomdomtr  6994  domsdomtr  6996  infdif  7835  ackbij1b  7865  isf32lem5  7983  alephreg  8204  cfpwsdom  8206  inar1  8397  tskcard  8403  npomex  8620  recnz  10087  rpnnen1lem5  10346  fznuz  10864  uznfz  10865  seqcoll2  11402  ramub1lem1  13073  pgpfac1lem1  15309  lsppratlem6  15905  nconsubb  17149  iunconlem  17153  clscon  17156  xkohaus  17347  reconnlem1  18331  ivthlem2  18812  perfectlem1  20468  lgseisenlem1  20588  ex-natded5.8-2  20801  erdszelem9  23141  heiborlem8  25954  lcvntr  28589  ncvr1  28835  llnneat  29076  2atnelpln  29106  lplnneat  29107  lplnnelln  29108  3atnelvolN  29148  lvolneatN  29150  lvolnelln  29151  lvolnelpln  29152  lplncvrlvol  29178  4atexlemntlpq  29630  cdleme0nex  29852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator