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  9128  domsdomtr  9130  infdif  10226  ackbij1b  10256  isf32lem5  10374  alephreg  10599  cfpwsdom  10601  inar1  10792  tskcard  10798  npomex  11013  recnz  12661  rpnnen1lem5  12989  fznuz  13609  uznfz  13610  seqcoll2  14452  ramub1lem1  16988  pgpfac1lem1  20024  lsppratlem6  21033  nconnsubb  23320  iunconnlem  23324  clsconn  23327  xkohaus  23550  reconnlem1  24735  ivthlem2  25374  perfectlem1  27155  lgseisenlem1  27301  ex-natded5.8-2  30217  oddpwdc  33964  erdszelem9  34799  relowlpssretop  36833  sucneqond  36834  heiborlem8  37280  lcvntr  38487  ncvr1  38733  llnneat  38976  2atnelpln  39006  lplnneat  39007  lplnnelln  39008  3atnelvolN  39048  lvolneatN  39050  lvolnelln  39051  lvolnelpln  39052  lplncvrlvol  39078  4atexlemntlpq  39530  cdleme0nex  39752  nlimsuc  42843