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  8400  sdomdomtr  9113  domsdomtr  9115  infdif  10267  ackbij1b  10297  isf32lem5  10416  alephreg  10648  cfpwsdom  10650  inar1  10841  tskcard  10847  npomex  11062  recnz  12755  rpnnen1lem5  13090  fznuz  13723  uznfz  13724  seqcoll2  14590  ramub1lem1  17184  chnccat  18780  pgpfac1lem1  20270  lsppratlem6  21410  nconnsubb  23721  iunconnlem  23725  clsconn  23728  xkohaus  23952  reconnlem1  25126  ivthlem2  25753  perfectlem1  27538  lgseisenlem1  27684  ex-natded5.8-2  30997  oddpwdc  34969  fineqvinfep  35766  erdszelem9  35933  relowlpssretop  38255  sucneqond  38256  heiborlem8  38720  lcvntr  40051  ncvr1  40297  llnneat  40539  2atnelpln  40569  lplnneat  40570  lplnnelln  40571  3atnelvolN  40611  lvolneatN  40613  lvolnelln  40614  lvolnelpln  40615  lplncvrlvol  40641  4atexlemntlpq  41093  cdleme0nex  41315  nlimsuc  44400