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  8404  sdomdomtr  9108  domsdomtr  9110  infdif  10210  ackbij1b  10240  isf32lem5  10359  alephreg  10585  cfpwsdom  10587  inar1  10778  tskcard  10784  npomex  10999  recnz  12689  rpnnen1lem5  13023  fznuz  13656  uznfz  13657  seqcoll2  14522  ramub1lem1  17111  chnccat  18707  pgpfac1lem1  20177  lsppratlem6  21313  nconnsubb  23617  iunconnlem  23621  clsconn  23624  xkohaus  23847  reconnlem1  25021  ivthlem2  25648  perfectlem1  27430  lgseisenlem1  27576  ex-natded5.8-2  30802  oddpwdc  34776  fineqvinfep  35562  erdszelem9  35712  relowlpssretop  38051  sucneqond  38052  heiborlem8  38510  lcvntr  39841  ncvr1  40087  llnneat  40329  2atnelpln  40359  lplnneat  40360  lplnnelln  40361  3atnelvolN  40401  lvolneatN  40403  lvolnelln  40404  lvolnelpln  40405  lplncvrlvol  40431  4atexlemntlpq  40883  cdleme0nex  41105  nlimsuc  44208