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  23730  heiborlem8  26542  lcvntr  29216  ncvr1  29462  llnneat  29703  2atnelpln  29733  lplnneat  29734  lplnnelln  29735  3atnelvolN  29775  lvolneatN  29777  lvolnelln  29778  lvolnelpln  29779  lplncvrlvol  29805  4atexlemntlpq  30257  cdleme0nex  30479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator