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  8033  sdomdomtr  8638  domsdomtr  8640  infdif  9619  ackbij1b  9649  isf32lem5  9767  alephreg  9992  cfpwsdom  9994  inar1  10185  tskcard  10191  npomex  10406  recnz  12045  rpnnen1lem5  12368  fznuz  12977  uznfz  12978  seqcoll2  13811  ramub1lem1  16350  pgpfac1lem1  19125  lsppratlem6  19853  nconnsubb  21959  iunconnlem  21963  clsconn  21966  xkohaus  22189  reconnlem1  23361  ivthlem2  23980  perfectlem1  25732  lgseisenlem1  25878  ex-natded5.8-2  28120  oddpwdc  31511  erdszelem9  32343  relowlpssretop  34527  sucneqond  34528  heiborlem8  34977  lcvntr  36042  ncvr1  36288  llnneat  36530  2atnelpln  36560  lplnneat  36561  lplnnelln  36562  3atnelvolN  36602  lvolneatN  36604  lvolnelln  36605  lvolnelpln  36606  lplncvrlvol  36632  4atexlemntlpq  37084  cdleme0nex  37306
  Copyright terms: Public domain W3C validator