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  8414  sdomdomtr  9116  domsdomtr  9118  infdif  10210  ackbij1b  10240  isf32lem5  10358  alephreg  10583  cfpwsdom  10585  inar1  10776  tskcard  10782  npomex  10997  recnz  12644  rpnnen1lem5  12972  fznuz  13590  uznfz  13591  seqcoll2  14433  ramub1lem1  16966  pgpfac1lem1  19992  lsppratlem6  20999  nconnsubb  23247  iunconnlem  23251  clsconn  23254  xkohaus  23477  reconnlem1  24662  ivthlem2  25301  perfectlem1  27075  lgseisenlem1  27221  ex-natded5.8-2  30100  oddpwdc  33817  erdszelem9  34654  relowlpssretop  36709  sucneqond  36710  heiborlem8  37150  lcvntr  38360  ncvr1  38606  llnneat  38849  2atnelpln  38879  lplnneat  38880  lplnnelln  38881  3atnelvolN  38921  lvolneatN  38923  lvolnelln  38924  lvolnelpln  38925  lplncvrlvol  38951  4atexlemntlpq  39403  cdleme0nex  39625  nlimsuc  42655