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  7450  sdomdomtr  8038  domsdomtr  8040  infdif  8976  ackbij1b  9006  isf32lem5  9124  alephreg  9349  cfpwsdom  9351  inar1  9542  tskcard  9548  npomex  9763  recnz  11396  rpnnen1lem5  11762  rpnnen1lem5OLD  11768  fznuz  12360  uznfz  12361  seqcoll2  13184  ramub1lem1  15649  pgpfac1lem1  18389  lsppratlem6  19066  nconnsubb  21131  iunconnlem  21135  clsconn  21138  xkohaus  21361  reconnlem1  22532  ivthlem2  23123  perfectlem1  24849  lgseisenlem1  24995  ex-natded5.8-2  27119  oddpwdc  30189  erdszelem9  30881  relowlpssretop  32817  sucneqond  32818  heiborlem8  33216  lcvntr  33760  ncvr1  34006  llnneat  34247  2atnelpln  34277  lplnneat  34278  lplnnelln  34279  3atnelvolN  34319  lvolneatN  34321  lvolnelln  34322  lvolnelpln  34323  lplncvrlvol  34349  4atexlemntlpq  34801  cdleme0nex  35024
  Copyright terms: Public domain W3C validator