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  8339  sdomdomtr  9038  domsdomtr  9040  infdif  10118  ackbij1b  10148  isf32lem5  10267  alephreg  10493  cfpwsdom  10495  inar1  10686  tskcard  10692  npomex  10907  recnz  12567  rpnnen1lem5  12894  fznuz  13525  uznfz  13526  seqcoll2  14388  ramub1lem1  16954  chnccat  18549  pgpfac1lem1  20005  lsppratlem6  21107  nconnsubb  23367  iunconnlem  23371  clsconn  23374  xkohaus  23597  reconnlem1  24771  ivthlem2  25409  perfectlem1  27196  lgseisenlem1  27342  ex-natded5.8-2  30489  oddpwdc  34511  fineqvinfep  35281  erdszelem9  35393  relowlpssretop  37565  sucneqond  37566  heiborlem8  38015  lcvntr  39282  ncvr1  39528  llnneat  39770  2atnelpln  39800  lplnneat  39801  lplnnelln  39802  3atnelvolN  39842  lvolneatN  39844  lvolnelln  39845  lvolnelpln  39846  lplncvrlvol  39872  4atexlemntlpq  40324  cdleme0nex  40546  nlimsuc  43678