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

Theorem mt2d 129
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 127 . 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  130  nsyl3  131  tz7.44-3  7271  sdomdomtr  7858  domsdomtr  7860  infdif  8794  ackbij1b  8824  isf32lem5  8942  alephreg  9163  cfpwsdom  9165  inar1  9356  tskcard  9362  npomex  9577  recnz  11196  rpnnen1lem5  11564  rpnnen1lem5OLD  11570  fznuz  12163  uznfz  12164  seqcoll2  12975  ramub1lem1  15456  pgpfac1lem1  18207  lsppratlem6  18881  nconsubb  20943  iunconlem  20947  clscon  20950  xkohaus  21173  reconnlem1  22350  ivthlem2  22907  perfectlem1  24647  lgseisenlem1  24793  ex-natded5.8-2  26405  oddpwdc  29554  erdszelem9  30284  relowlpssretop  32223  sucneqond  32224  heiborlem8  32681  lcvntr  33225  ncvr1  33471  llnneat  33712  2atnelpln  33742  lplnneat  33743  lplnnelln  33744  3atnelvolN  33784  lvolneatN  33786  lvolnelln  33787  lvolnelpln  33788  lplncvrlvol  33814  4atexlemntlpq  34266  cdleme0nex  34489
  Copyright terms: Public domain W3C validator