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

Theorem mt2d 131
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 129 . 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  132  nsyl3  133  tz7.44-3  7549  sdomdomtr  8134  domsdomtr  8136  infdif  9069  ackbij1b  9099  isf32lem5  9217  alephreg  9442  cfpwsdom  9444  inar1  9635  tskcard  9641  npomex  9856  recnz  11490  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  fznuz  12460  uznfz  12461  seqcoll2  13287  ramub1lem1  15777  pgpfac1lem1  18519  lsppratlem6  19200  nconnsubb  21274  iunconnlem  21278  clsconn  21281  xkohaus  21504  reconnlem1  22676  ivthlem2  23267  perfectlem1  24999  lgseisenlem1  25145  ex-natded5.8-2  27401  oddpwdc  30544  erdszelem9  31307  relowlpssretop  33342  sucneqond  33343  heiborlem8  33747  lcvntr  34631  ncvr1  34877  llnneat  35118  2atnelpln  35148  lplnneat  35149  lplnnelln  35150  3atnelvolN  35190  lvolneatN  35192  lvolnelln  35193  lvolnelpln  35194  lplncvrlvol  35220  4atexlemntlpq  35672  cdleme0nex  35895
  Copyright terms: Public domain W3C validator