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

Theorem mt2d 123
Description: Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
Hypotheses
Ref Expression
mt2d.1 (𝜑𝜒)
mt2d.2 (𝜑 → (𝜓 → ¬ 𝜒))
Assertion
Ref Expression
mt2d (𝜑 → ¬ 𝜓)

Proof of Theorem mt2d
StepHypRef Expression
1 mt2d.1 . 2 (𝜑𝜒)
2 mt2d.2 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
32con2d 121 . 2 (𝜑 → (𝜒 → ¬ 𝜓))
41, 3mpd 15 1 (𝜑 → ¬ 𝜓)
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  124  nsyl3  125  tz7.44-3  7203  sdomdomtr  7789  domsdomtr  7791  infdif  8724  ackbij1b  8754  isf32lem5  8872  alephreg  9092  cfpwsdom  9094  inar1  9285  tskcard  9291  npomex  9506  recnz  11101  rpnnen1lem5  11385  fznuz  11974  uznfz  11975  seqcoll2  12751  ramub1lem1  15146  pgpfac1lem1  17867  lsppratlem6  18535  nconsubb  20595  iunconlem  20599  clscon  20602  xkohaus  20825  reconnlem1  22002  ivthlem2  22562  perfectlem1  24318  lgseisenlem1  24438  ex-natded5.8-2  26024  oddpwdc  29341  erdszelem9  30074  relowlpssretop  31988  sucneqond  31989  heiborlem8  32387  lcvntr  32832  ncvr1  33078  llnneat  33319  2atnelpln  33349  lplnneat  33350  lplnnelln  33351  3atnelvolN  33391  lvolneatN  33393  lvolnelln  33394  lvolnelpln  33395  lplncvrlvol  33421  4atexlemntlpq  33873  cdleme0nex  34096
  Copyright terms: Public domain W3C validator