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  8376  sdomdomtr  9074  domsdomtr  9076  infdif  10161  ackbij1b  10191  isf32lem5  10310  alephreg  10535  cfpwsdom  10537  inar1  10728  tskcard  10734  npomex  10949  recnz  12609  rpnnen1lem5  12940  fznuz  13570  uznfz  13571  seqcoll2  14430  ramub1lem1  16997  pgpfac1lem1  20006  lsppratlem6  21062  nconnsubb  23310  iunconnlem  23314  clsconn  23317  xkohaus  23540  reconnlem1  24715  ivthlem2  25353  perfectlem1  27140  lgseisenlem1  27286  ex-natded5.8-2  30343  oddpwdc  34345  erdszelem9  35186  relowlpssretop  37352  sucneqond  37353  heiborlem8  37812  lcvntr  39019  ncvr1  39265  llnneat  39508  2atnelpln  39538  lplnneat  39539  lplnnelln  39540  3atnelvolN  39580  lvolneatN  39582  lvolnelln  39583  lvolnelpln  39584  lplncvrlvol  39610  4atexlemntlpq  40062  cdleme0nex  40284  nlimsuc  43430