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  8349  sdomdomtr  9050  domsdomtr  9052  infdif  10130  ackbij1b  10160  isf32lem5  10279  alephreg  10505  cfpwsdom  10507  inar1  10698  tskcard  10704  npomex  10919  recnz  12579  rpnnen1lem5  12906  fznuz  13537  uznfz  13538  seqcoll2  14400  ramub1lem1  16966  chnccat  18561  pgpfac1lem1  20017  lsppratlem6  21119  nconnsubb  23379  iunconnlem  23383  clsconn  23386  xkohaus  23609  reconnlem1  24783  ivthlem2  25421  perfectlem1  27208  lgseisenlem1  27354  ex-natded5.8-2  30501  oddpwdc  34531  fineqvinfep  35300  erdszelem9  35412  relowlpssretop  37613  sucneqond  37614  heiborlem8  38063  lcvntr  39396  ncvr1  39642  llnneat  39884  2atnelpln  39914  lplnneat  39915  lplnnelln  39916  3atnelvolN  39956  lvolneatN  39958  lvolnelln  39959  lvolnelpln  39960  lplncvrlvol  39986  4atexlemntlpq  40438  cdleme0nex  40660  nlimsuc  43791