Theorem mt2d 136

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

Step	Hyp	Ref	Expression
1		mt2d.1	. 2 ⊢ (𝜑 → 𝜒)
2		mt2d.2	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	2	con2d 134	. 2 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))
4	1, 3	mpd 15	1 ⊢ (𝜑 → ¬ 𝜓)

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  137  nsyl3  138  tz7.44-3  8464  sdomdomtr  9176  domsdomtr  9178  infdif  10277  ackbij1b  10307  isf32lem5  10426  alephreg  10651  cfpwsdom  10653  inar1  10844  tskcard  10850  npomex  11065  recnz  12718  rpnnen1lem5  13046  fznuz  13666  uznfz  13667  seqcoll2  14514  ramub1lem1  17073  pgpfac1lem1  20118  lsppratlem6  21177  nconnsubb  23452  iunconnlem  23456  clsconn  23459  xkohaus  23682  reconnlem1  24867  ivthlem2  25506  perfectlem1  27291  lgseisenlem1  27437  ex-natded5.8-2  30446  oddpwdc  34319  erdszelem9  35167  relowlpssretop  37330  sucneqond  37331  heiborlem8  37778  lcvntr  38982  ncvr1  39228  llnneat  39471  2atnelpln  39501  lplnneat  39502  lplnnelln  39503  3atnelvolN  39543  lvolneatN  39545  lvolnelln  39546  lvolnelpln  39547  lplncvrlvol  39573  4atexlemntlpq  40025  cdleme0nex  40247  nlimsuc  43403