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

Theorem mt2d 138
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 136 . 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  139  nsyl3  140  tz7.44-3  8035  sdomdomtr  8639  domsdomtr  8641  infdif  9620  ackbij1b  9650  isf32lem5  9768  alephreg  9993  cfpwsdom  9995  inar1  10186  tskcard  10192  npomex  10407  recnz  12046  rpnnen1lem5  12370  fznuz  12979  uznfz  12980  seqcoll2  13813  ramub1lem1  16352  pgpfac1lem1  19116  lsppratlem6  19844  nconnsubb  21947  iunconnlem  21951  clsconn  21954  xkohaus  22177  reconnlem1  23349  ivthlem2  23968  perfectlem1  25719  lgseisenlem1  25865  ex-natded5.8-2  28107  oddpwdc  31498  erdszelem9  32330  relowlpssretop  34514  sucneqond  34515  heiborlem8  34964  lcvntr  36029  ncvr1  36275  llnneat  36517  2atnelpln  36547  lplnneat  36548  lplnnelln  36549  3atnelvolN  36589  lvolneatN  36591  lvolnelln  36592  lvolnelpln  36593  lplncvrlvol  36619  4atexlemntlpq  37071  cdleme0nex  37293
  Copyright terms: Public domain W3C validator