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

Theorem mt2d 120
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 118 . 2  |-  ( ph  ->  ( ch  ->  -.  ps ) )
41, 3mpd 15 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt2i  121  nsyl3  122  tz7.44-3  7134  sdomdomtr  7711  domsdomtr  7713  infdif  8637  ackbij1b  8667  isf32lem5  8785  alephreg  9005  cfpwsdom  9007  inar1  9199  tskcard  9205  npomex  9420  recnz  11011  rpnnen1lem5  11294  fznuz  11874  uznfz  11875  seqcoll2  12622  ramub1lem1  14938  pgpfac1lem1  17633  lsppratlem6  18301  nconsubb  20360  iunconlem  20364  clscon  20367  xkohaus  20590  reconnlem1  21746  ivthlem2  22275  perfectlem1  24011  lgseisenlem1  24131  ex-natded5.8-2  25700  oddpwdc  29004  erdszelem9  29701  relowlpssretop  31492  heiborlem8  31844  lcvntr  32291  ncvr1  32537  llnneat  32778  2atnelpln  32808  lplnneat  32809  lplnnelln  32810  3atnelvolN  32850  lvolneatN  32852  lvolnelln  32853  lvolnelpln  32854  lplncvrlvol  32880  4atexlemntlpq  33332  cdleme0nex  33555
  Copyright terms: Public domain W3C validator