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  8422  sdomdomtr  9124  domsdomtr  9126  infdif  10222  ackbij1b  10252  isf32lem5  10371  alephreg  10596  cfpwsdom  10598  inar1  10789  tskcard  10795  npomex  11010  recnz  12668  rpnnen1lem5  12997  fznuz  13626  uznfz  13627  seqcoll2  14483  ramub1lem1  17046  pgpfac1lem1  20057  lsppratlem6  21113  nconnsubb  23361  iunconnlem  23365  clsconn  23368  xkohaus  23591  reconnlem1  24766  ivthlem2  25405  perfectlem1  27192  lgseisenlem1  27338  ex-natded5.8-2  30395  oddpwdc  34386  erdszelem9  35221  relowlpssretop  37382  sucneqond  37383  heiborlem8  37842  lcvntr  39044  ncvr1  39290  llnneat  39533  2atnelpln  39563  lplnneat  39564  lplnnelln  39565  3atnelvolN  39605  lvolneatN  39607  lvolnelln  39608  lvolnelpln  39609  lplncvrlvol  39635  4atexlemntlpq  40087  cdleme0nex  40309  nlimsuc  43465