Theorem mt2d 137

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 135	. 2 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))
4	1, 3	mpd 16	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mt2i  138  nsyl3  139  tz7.44-3  8444  sdomdomtr  9157  domsdomtr  9159  infdif  10313  ackbij1b  10343  isf32lem5  10462  alephreg  10694  cfpwsdom  10696  inar1  10887  tskcard  10893  npomex  11108  recnz  12801  rpnnen1lem5  13136  fznuz  13770  uznfz  13771  seqcoll2  14637  ramub1lem1  17233  chnccat  18829  pgpfac1lem1  20320  lsppratlem6  21460  nconnsubb  23771  iunconnlem  23775  clsconn  23778  xkohaus  24002  reconnlem1  25176  ivthlem2  25803  perfectlem1  27586  lgseisenlem1  27732  ex-natded5.8-2  31045  oddpwdc  35056  fineqvinfep  35893  erdszelem9  36131  relowlpssretop  38479  sucneqond  38480  heiborlem8  38944  lcvntr  40275  ncvr1  40521  llnneat  40763  2atnelpln  40793  lplnneat  40794  lplnnelln  40795  3atnelvolN  40835  lvolneatN  40837  lvolnelln  40838  lvolnelpln  40839  lplncvrlvol  40865  4atexlemntlpq  41317  cdleme0nex  41539  nlimsuc  44634