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  8419  sdomdomtr  9132  domsdomtr  9134  infdif  10289  ackbij1b  10319  isf32lem5  10438  alephreg  10670  cfpwsdom  10672  inar1  10863  tskcard  10869  npomex  11084  recnz  12777  rpnnen1lem5  13112  fznuz  13746  uznfz  13747  seqcoll2  14613  ramub1lem1  17209  chnccat  18805  pgpfac1lem1  20295  lsppratlem6  21435  nconnsubb  23746  iunconnlem  23750  clsconn  23753  xkohaus  23977  reconnlem1  25151  ivthlem2  25778  perfectlem1  27561  lgseisenlem1  27707  ex-natded5.8-2  31020  oddpwdc  35032  fineqvinfep  35849  erdszelem9  36050  relowlpssretop  38380  sucneqond  38381  heiborlem8  38845  lcvntr  40176  ncvr1  40422  llnneat  40664  2atnelpln  40694  lplnneat  40695  lplnnelln  40696  3atnelvolN  40736  lvolneatN  40738  lvolnelln  40739  lvolnelpln  40740  lplncvrlvol  40766  4atexlemntlpq  41218  cdleme0nex  41440  nlimsuc  44535