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  8374  sdomdomtr  9078  domsdomtr  9080  infdif  10161  ackbij1b  10191  isf32lem5  10311  alephreg  10537  cfpwsdom  10539  inar1  10730  tskcard  10736  npomex  10951  recnz  12645  rpnnen1lem5  12979  fznuz  13611  uznfz  13612  seqcoll2  14475  ramub1lem1  17045  chnccat  18641  pgpfac1lem1  20099  lsppratlem6  21202  nconnsubb  23463  iunconnlem  23467  clsconn  23470  xkohaus  23693  reconnlem1  24867  ivthlem2  25494  perfectlem1  27270  lgseisenlem1  27416  ex-natded5.8-2  30562  oddpwdc  34612  fineqvinfep  35385  erdszelem9  35513  relowlpssretop  37822  sucneqond  37823  heiborlem8  38281  lcvntr  39614  ncvr1  39860  llnneat  40102  2atnelpln  40132  lplnneat  40133  lplnnelln  40134  3atnelvolN  40174  lvolneatN  40176  lvolnelln  40177  lvolnelpln  40178  lplncvrlvol  40204  4atexlemntlpq  40656  cdleme0nex  40878  nlimsuc  43981