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

Theorem mt2d 133
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 131 . 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  134  nsyl3  135  tz7.44-3  7658  sdomdomtr  8250  domsdomtr  8252  infdif  9234  ackbij1b  9264  isf32lem5  9382  alephreg  9607  cfpwsdom  9609  inar1  9800  tskcard  9806  npomex  10021  recnz  11655  rpnnen1lem5  12022  rpnnen1lem5OLD  12028  fznuz  12630  uznfz  12631  seqcoll2  13452  ramub1lem1  15938  pgpfac1lem1  18682  lsppratlem6  19368  nconnsubb  21448  iunconnlem  21452  clsconn  21455  xkohaus  21678  reconnlem1  22850  ivthlem2  23441  perfectlem1  25176  lgseisenlem1  25322  ex-natded5.8-2  27614  oddpwdc  30757  erdszelem9  31520  relowlpssretop  33550  sucneqond  33551  heiborlem8  33950  lcvntr  34836  ncvr1  35082  llnneat  35323  2atnelpln  35353  lplnneat  35354  lplnnelln  35355  3atnelvolN  35395  lvolneatN  35397  lvolnelln  35398  lvolnelpln  35399  lplncvrlvol  35425  4atexlemntlpq  35877  cdleme0nex  36100
  Copyright terms: Public domain W3C validator