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  8379  sdomdomtr  9080  domsdomtr  9082  infdif  10168  ackbij1b  10198  isf32lem5  10317  alephreg  10542  cfpwsdom  10544  inar1  10735  tskcard  10741  npomex  10956  recnz  12616  rpnnen1lem5  12947  fznuz  13577  uznfz  13578  seqcoll2  14437  ramub1lem1  17004  pgpfac1lem1  20013  lsppratlem6  21069  nconnsubb  23317  iunconnlem  23321  clsconn  23324  xkohaus  23547  reconnlem1  24722  ivthlem2  25360  perfectlem1  27147  lgseisenlem1  27293  ex-natded5.8-2  30350  oddpwdc  34352  erdszelem9  35193  relowlpssretop  37359  sucneqond  37360  heiborlem8  37819  lcvntr  39026  ncvr1  39272  llnneat  39515  2atnelpln  39545  lplnneat  39546  lplnnelln  39547  3atnelvolN  39587  lvolneatN  39589  lvolnelln  39590  lvolnelpln  39591  lplncvrlvol  39617  4atexlemntlpq  40069  cdleme0nex  40291  nlimsuc  43437