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  7368  sdomdomtr  7955  domsdomtr  7957  infdif  8891  ackbij1b  8921  isf32lem5  9039  alephreg  9260  cfpwsdom  9262  inar1  9453  tskcard  9459  npomex  9674  recnz  11284  rpnnen1lem5  11650  rpnnen1lem5OLD  11656  fznuz  12246  uznfz  12247  seqcoll2  13058  ramub1lem1  15514  pgpfac1lem1  18242  lsppratlem6  18919  nconsubb  20978  iunconlem  20982  clscon  20985  xkohaus  21208  reconnlem1  22369  ivthlem2  22945  perfectlem1  24671  lgseisenlem1  24817  ex-natded5.8-2  26429  oddpwdc  29549  erdszelem9  30241  relowlpssretop  32184  sucneqond  32185  heiborlem8  32583  lcvntr  33127  ncvr1  33373  llnneat  33614  2atnelpln  33644  lplnneat  33645  lplnnelln  33646  3atnelvolN  33686  lvolneatN  33688  lvolnelln  33689  lvolnelpln  33690  lplncvrlvol  33716  4atexlemntlpq  34168  cdleme0nex  34391
  Copyright terms: Public domain W3C validator