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  8405  sdomdomtr  9107  domsdomtr  9109  infdif  10201  ackbij1b  10231  isf32lem5  10349  alephreg  10574  cfpwsdom  10576  inar1  10767  tskcard  10773  npomex  10988  recnz  12634  rpnnen1lem5  12962  fznuz  13580  uznfz  13581  seqcoll2  14423  ramub1lem1  16956  pgpfac1lem1  19939  lsppratlem6  20758  nconnsubb  22919  iunconnlem  22923  clsconn  22926  xkohaus  23149  reconnlem1  24334  ivthlem2  24961  perfectlem1  26722  lgseisenlem1  26868  ex-natded5.8-2  29657  oddpwdc  33342  erdszelem9  34179  relowlpssretop  36234  sucneqond  36235  heiborlem8  36675  lcvntr  37885  ncvr1  38131  llnneat  38374  2atnelpln  38404  lplnneat  38405  lplnnelln  38406  3atnelvolN  38446  lvolneatN  38448  lvolnelln  38449  lvolnelpln  38450  lplncvrlvol  38476  4atexlemntlpq  38928  cdleme0nex  39150  nlimsuc  42178