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  8447  sdomdomtr  9149  domsdomtr  9151  infdif  10246  ackbij1b  10276  isf32lem5  10395  alephreg  10620  cfpwsdom  10622  inar1  10813  tskcard  10819  npomex  11034  recnz  12691  rpnnen1lem5  13021  fznuz  13646  uznfz  13647  seqcoll2  14501  ramub1lem1  17060  pgpfac1lem1  20109  lsppratlem6  21172  nconnsubb  23447  iunconnlem  23451  clsconn  23454  xkohaus  23677  reconnlem1  24862  ivthlem2  25501  perfectlem1  27288  lgseisenlem1  27434  ex-natded5.8-2  30443  oddpwdc  34336  erdszelem9  35184  relowlpssretop  37347  sucneqond  37348  heiborlem8  37805  lcvntr  39008  ncvr1  39254  llnneat  39497  2atnelpln  39527  lplnneat  39528  lplnnelln  39529  3atnelvolN  39569  lvolneatN  39571  lvolnelln  39572  lvolnelpln  39573  lplncvrlvol  39599  4atexlemntlpq  40051  cdleme0nex  40273  nlimsuc  43431